Langlib

Langlib.Classes.ContextFree.Examples.A2nBnPosStar

Imports

Init
Langlib.Examples.A2nBnPosStar
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.Star
Langlib.Classes.ContextFree.Examples.A2nBnPos
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_quotientNumerator

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

theorem CF_quotientNumerator :

is_CF quotientNumerator