Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-05 19:36 427aae3a

View on Github →

chore(algebra/*): generalisation linter (replacing ring with non_assoc_ring) (#13106)

Estimated changes

Modified src/algebra/big_operators/multiset.lean

Modified src/algebra/big_operators/pi.lean

modified theorem ring_hom.functions_ext

Modified src/algebra/big_operators/ring.lean

Modified src/algebra/char_zero.lean

Modified src/algebra/group_power/lemmas.lean

modified theorem bit0_mul

modified theorem bit1_mul

modified theorem mul_bit0

modified theorem mul_bit1

modified theorem nsmul_eq_mul'

modified theorem nsmul_eq_mul

modified theorem zsmul_eq_mul

Modified src/algebra/ring/equiv.lean

Modified src/ring_theory/subring/basic.lean