Commit 2025-02-11 19:55 42d848cf

View on Github →

chore(Algebra/Ring): process porting notes (#21723)

Estimated changes

Modified Mathlib/Algebra/Ring/Action/Invariant.lean

Modified Mathlib/Algebra/Ring/CentroidHom.lean

Modified Mathlib/Algebra/Ring/Defs.lean

Modified Mathlib/Algebra/Ring/Divisibility/Basic.lean

modified theorem dvd_sub_comm

Modified Mathlib/Algebra/Ring/Equiv.lean

Modified Mathlib/Algebra/Ring/Hom/Defs.lean

Modified Mathlib/Algebra/Ring/Parity.lean

Modified Mathlib/Algebra/Ring/Subsemiring/Basic.lean

Modified Mathlib/Algebra/Ring/Subsemiring/Defs.lean

Modified Mathlib/FieldTheory/Fixed.lean