Commit 2023-03-25 12:28 525ff058

View on Github →

feat: port Algebra.MonoidAlgebra.Division (#3068) This is the second part of the forward port of leanprover-community/mathlib#15905.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/MonoidAlgebra/Division.lean

added theorem AddMonoidAlgebra.add_divOf

added theorem AddMonoidAlgebra.divOf_add

added theorem AddMonoidAlgebra.divOf_add_modOf

added theorem AddMonoidAlgebra.divOf_apply

added theorem AddMonoidAlgebra.divOf_zero

added theorem AddMonoidAlgebra.modOf_add_divOf

added theorem AddMonoidAlgebra.modOf_apply_add_self

added theorem AddMonoidAlgebra.modOf_apply_of_exists_add

added theorem AddMonoidAlgebra.modOf_apply_of_not_exists_add

added theorem AddMonoidAlgebra.modOf_apply_self_add

added theorem AddMonoidAlgebra.mul_of'_divOf

added theorem AddMonoidAlgebra.mul_of'_modOf

added theorem AddMonoidAlgebra.of'_divOf

added theorem AddMonoidAlgebra.of'_dvd_iff_modOf_eq_zero

added theorem AddMonoidAlgebra.of'_modOf

added theorem AddMonoidAlgebra.of'_mul_divOf

added theorem AddMonoidAlgebra.of'_mul_modOf

added theorem AddMonoidAlgebra.support_divOf

added theorem AddMonoidAlgebra.zero_divOf