Commit 2024-12-27 11:03 6ab855d1

View on Github →

chore: rename MulEquiv.mulEquivOfUnique to MulEquiv.ofUnique (#20243)

Estimated changes

Modified Mathlib/Algebra/GCDMonoid/Basic.lean

Modified Mathlib/Algebra/Group/Equiv/Basic.lean

deleted def MulEquiv.mulEquivOfUnique

added def MulEquiv.ofUnique

Modified Mathlib/Algebra/Ring/Equiv.lean

added def RingEquiv.ofUnique

deleted def RingEquiv.ringEquivOfUnique

Modified Mathlib/CategoryTheory/Limits/Shapes/Types.lean

Modified Mathlib/Data/FinEnum.lean

Modified Mathlib/GroupTheory/Perm/Cycle/Type.lean

Modified Mathlib/LinearAlgebra/Dimension/Free.lean

Modified Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean

Modified Mathlib/Logic/Equiv/Basic.lean

Modified Mathlib/Logic/Equiv/Defs.lean

deleted def Equiv.equivOfUnique

modified def Equiv.equivPUnit

added def Equiv.ofUnique

Modified Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean

Modified Mathlib/Order/Estimator.lean

Modified Mathlib/Order/RelIso/Basic.lean

added def RelIso.ofUniqueOfIrrefl

added def RelIso.ofUniqueOfRefl

deleted def RelIso.relIsoOfUniqueOfIrrefl

deleted def RelIso.relIsoOfUniqueOfRefl

Modified Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean

Modified Mathlib/RingTheory/DedekindDomain/Ideal.lean

Modified Mathlib/SetTheory/Cardinal/Basic.lean

Modified Mathlib/SetTheory/Game/Nim.lean

Modified Mathlib/SetTheory/Game/Ordinal.lean

Modified Mathlib/SetTheory/Ordinal/Basic.lean

Modified Mathlib/Topology/Homeomorph.lean