Commit 2025-09-20 08:39 9803e9a3

View on Github →

feat(Algebra): preliminaries for ring structure on AddLocalization (#29597)

Estimated changes

Modified Mathlib/Algebra/Module/End.lean

modified theorem IsAddUnit.smul_left

Modified Mathlib/Algebra/Order/Nonneg/Basic.lean

Modified Mathlib/Algebra/Order/Nonneg/Ring.lean

Modified Mathlib/Algebra/Ring/Invertible.lean

added def AddUnits.mulLeft

added def AddUnits.mulRight

added theorem AddUnits.neg_mul_eq_mul_neg

added theorem AddUnits.neg_mul_left

added theorem AddUnits.neg_mul_neg

added theorem AddUnits.neg_mul_right

added theorem IsAddUnit.mul_left

added theorem IsAddUnit.mul_right

Modified Mathlib/LinearAlgebra/TensorProduct/Basic.lean

added theorem IsAddUnit.tmul_left

added theorem IsAddUnit.tmul_right