Commit 2024-10-09 16:54 4034bcf9

View on Github →

chore: remove some Setoid.r (#16258)

Estimated changes

Modified Counterexamples/CliffordAlgebraNotInjective.lean

Modified Mathlib/Algebra/Lie/Quotient.lean

Modified Mathlib/Computability/Reduce.lean

Modified Mathlib/Data/List/Rotate.lean

Modified Mathlib/Data/Quot.lean

modified theorem Quotient.mk_out'

modified theorem Quotient.sound'

Modified Mathlib/Data/Setoid/Partition.lean

Modified Mathlib/GroupTheory/Coset/Basic.lean

modified theorem QuotientGroup.leftRel_apply

modified theorem QuotientGroup.leftRel_eq

modified theorem QuotientGroup.rightRel_apply

modified theorem QuotientGroup.rightRel_eq

Modified Mathlib/GroupTheory/Index.lean

Modified Mathlib/GroupTheory/QuotientGroup/Basic.lean

Modified Mathlib/LinearAlgebra/InvariantBasisNumber.lean

Modified Mathlib/LinearAlgebra/Quotient.lean

added theorem Submodule.quotientRel_def

deleted theorem Submodule.quotientRel_r_def

Modified Mathlib/Logic/Equiv/Basic.lean

Modified Mathlib/Logic/Equiv/Defs.lean

Modified Mathlib/NumberTheory/RamificationInertia.lean

Modified Mathlib/RingTheory/AdicCompletion/Algebra.lean

Modified Mathlib/RingTheory/Ideal/Quotient.lean

Modified Mathlib/Topology/Algebra/UniformRing.lean

Modified Mathlib/Topology/Constructions.lean