Commit 2024-11-20 14:09 f02eb615

View on Github →

chore: deprecate Quotient.out' (#17941)

Estimated changes

Modified Mathlib/Data/Multiset/Basic.lean

Modified Mathlib/Data/Quot.lean

modified theorem Quotient.mk_out'

modified theorem Quotient.out_eq'

Modified Mathlib/Data/Setoid/Basic.lean

Modified Mathlib/Data/Setoid/Partition.lean

deleted theorem IndexedPartition.index_out'

added theorem IndexedPartition.index_out

Modified Mathlib/GroupTheory/Complement.lean

Modified Mathlib/GroupTheory/Coset/Basic.lean

deleted theorem QuotientGroup.orbit_eq_out'_smul

added theorem QuotientGroup.orbit_eq_out_smul

Modified Mathlib/GroupTheory/Coset/Defs.lean

deleted theorem QuotientGroup.mk_out'_eq_mul

added theorem QuotientGroup.mk_out_eq_mul

modified theorem QuotientGroup.out_eq'

Modified Mathlib/GroupTheory/DoubleCoset.lean

deleted theorem Doset.disjoint_out'

added theorem Doset.disjoint_out

deleted theorem Doset.mk_out'_eq_mul

added theorem Doset.mk_out_eq_mul

modified theorem Doset.out_eq'

Modified Mathlib/GroupTheory/GroupAction/Defs.lean

modified def MulAction.selfEquivSigmaOrbits

Modified Mathlib/GroupTheory/GroupAction/Quotient.lean

deleted theorem MulAction.Quotient.coe_smul_out'

added theorem MulAction.Quotient.coe_smul_out

deleted theorem MulAction.Quotient.mk_smul_out'

added theorem MulAction.Quotient.mk_smul_out

deleted theorem QuotientGroup.out'_conj_pow_minimalPeriod_mem

added theorem QuotientGroup.out_conj_pow_minimalPeriod_mem

Modified Mathlib/GroupTheory/Transfer.lean

Modified Mathlib/LinearAlgebra/Projectivization/Basic.lean

Modified Mathlib/MeasureTheory/Function/AEEqFun.lean

Modified Mathlib/MeasureTheory/Measure/Haar/Quotient.lean

Modified Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean

Modified Mathlib/Order/Antisymmetrization.lean

Modified Mathlib/Order/RelIso/Basic.lean

Modified Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean

Modified Mathlib/RingTheory/Ideal/Quotient/Basic.lean

Modified Mathlib/RingTheory/Perfection.lean

Modified Mathlib/Topology/Algebra/ClosedSubgroup.lean

Modified Mathlib/Topology/UniformSpace/Separation.lean