OAI/NumberTheory/Ostmann/Arithmetic/GroupHaarImage.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Ostmann.Arithmetic.GroupHaarImage.homProductEquivline 13 - theorem
OAI.Ostmann.Arithmetic.GroupHaarImage.average_surjectiveline 27 - theorem
OAI.Ostmann.Arithmetic.GroupHaarImage.average_rangeline 44