OAI/NumberTheory/Ostmann/Construction/DiagonalTransformFiber.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Ostmann.Construction.diagonalCoefficientTermline 17 - def
OAI.Ostmann.Construction.diagonalHalfTransformline 21 - lemma
OAI.Ostmann.Construction.remainingTermValue_eq_diagonalHalfTransform_mulline 28 - theorem
OAI.Ostmann.Construction.diagonalHalfTransform_eq_of_tagline 33 - theorem
OAI.Ostmann.Construction.diagonal_grouped_transform_factorline 50 - theorem
OAI.Ostmann.Construction.diagonal_grouped_square_le_smallMultiplierline 76