Commit 2024-05-23 07:03 9f012931

View on Github →

chore: Move Invertible (#13030) Move the material about Invertible to files under Algebra.Group, Algebra.GroupWithZero, Algebra.Ring.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Center.lean

Renamed Mathlib/Algebra/Invertible/Basic.lean to Mathlib/Algebra/Group/Invertible/Basic.lean

deleted theorem Ring.inverse_invertible

deleted theorem div_mul_cancel_of_invertible

deleted theorem div_self_of_invertible

deleted theorem invOf_div

deleted def invertibleDiv

deleted theorem mul_div_cancel_of_invertible

Renamed Mathlib/Algebra/Invertible/Defs.lean to Mathlib/Algebra/Group/Invertible/Defs.lean

Renamed Mathlib/Algebra/Invertible/GroupWithZero.lean to Mathlib/Algebra/GroupWithZero/Invertible.lean

added theorem Ring.inverse_invertible

added theorem div_mul_cancel_of_invertible

added theorem div_self_of_invertible

added theorem invOf_div

added def invertibleDiv

added theorem mul_div_cancel_of_invertible

Modified Mathlib/Algebra/Order/Invertible.lean

Renamed Mathlib/Algebra/Invertible/Ring.lean to Mathlib/Algebra/Ring/Invertible.lean

Modified Mathlib/Algebra/Star/Basic.lean

Modified Mathlib/GroupTheory/GroupAction/Group.lean

Modified Mathlib/Tactic/NormNum/Basic.lean

Modified Mathlib/Tactic/NormNum/Result.lean

Modified scripts/noshake.json