Langlib

Langlib.Classes.ContextFree.Examples.BnAnPosStarB

Imports

Init
Langlib.Examples.BnAnPosStarB
Mathlib.NumberTheory.LucasLehmer
Mathlib.NumberTheory.SelbergSieve
Langlib.Classes.ContextFree.Definition
Mathlib.Analysis.SpecialFunctions.Bernstein
Mathlib.CategoryTheory.Category.Init
Mathlib.Combinatorics.Enumerative.DyckWord
Mathlib.Data.NNRat.Floor
Mathlib.Geometry.Euclidean.Altitude
Mathlib.NumberTheory.Height.Basic
Mathlib.Tactic.NormNum.BigOperators
Mathlib.Tactic.NormNum.Irrational
Mathlib.Tactic.NormNum.IsCoprime
Mathlib.Tactic.NormNum.IsSquare
Mathlib.Tactic.NormNum.LegendreSymbol
Mathlib.Tactic.NormNum.ModEq
Mathlib.Tactic.NormNum.NatFactorial
Mathlib.Tactic.NormNum.NatFib
Mathlib.Tactic.NormNum.NatLog
Mathlib.Tactic.NormNum.NatSqrt
Mathlib.Tactic.NormNum.Ordinal
Mathlib.Tactic.NormNum.Parity
Mathlib.Tactic.NormNum.Prime
Mathlib.Tactic.NormNum.RealSqrt
Mathlib.Topology.Sheaves.Init
Langlib.Classes.ContextFree.Closure.Concatenation
Langlib.Classes.ContextFree.Closure.Homomorphism
Langlib.Classes.ContextFree.Closure.Star
Langlib.Classes.ContextFree.Examples.BnAnPos
Mathlib.Algebra.Order.Floor.Extended
Mathlib.Algebra.Order.Floor.Semifield
Mathlib.Algebra.Order.Interval.Basic
Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Mathlib.Data.Nat.Factorial.DoubleFactorial

Imported by

CF_quotientDenominator

The `{b^n a^n | n >= 1}* {b}` language #

theorem CF_quotientDenominator :

is_CF quotientDenominator