Commit 2024-08-05 12:37 38886f70

View on Github →

chore(GroupTheory/Coset): deprecate some lemma (#15482) They were different in mathlib3 because of coercions.

Estimated changes

Modified Mathlib/Algebra/Order/ToIntervalMod.lean

Modified Mathlib/Algebra/Pointwise/Stabilizer.lean

Modified Mathlib/Analysis/Fourier/AddCircle.lean

Modified Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean

Modified Mathlib/Data/ZMod/Quotient.lean

Modified Mathlib/GroupTheory/Commensurable.lean

Modified Mathlib/GroupTheory/Complement.lean

Modified Mathlib/GroupTheory/Coset.lean

deleted theorem QuotientGroup.eq'

deleted theorem QuotientGroup.induction_on'

Modified Mathlib/GroupTheory/GroupAction/Quotient.lean

Modified Mathlib/GroupTheory/QuotientGroup.lean

Modified Mathlib/GroupTheory/Torsion.lean

Modified Mathlib/LinearAlgebra/Alternating/DomCoprod.lean

Modified Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean

Modified Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean

Modified Mathlib/Topology/Instances/AddCircle.lean