Commit 2023-03-24 20:19 90fa71a5

View on Github →

chore: forward-port leanprover-community#15905 (#3059)

Estimated changes

Modified Mathlib/Algebra/MonoidAlgebra/Basic.lean

added theorem AddMonoidAlgebra.mul_single_apply_of_not_exists_add

added theorem AddMonoidAlgebra.single_mul_apply_of_not_exists_add

added theorem MonoidAlgebra.mul_single_apply_of_not_exists_mul

added theorem MonoidAlgebra.single_mul_apply_of_not_exists_mul