Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-01 10:46 6652766b

View on Github →

chore(algebra/ring/basic): generalisation linter (#13094)

Estimated changes

Modified src/algebra/ring/basic.lean

modified theorem boole_mul

modified theorem commute.bit1_left

modified theorem commute.bit1_right

modified theorem distrib_three_right

modified theorem is_left_regular_of_non_zero_divisor

modified theorem is_right_regular_of_non_zero_divisor

modified theorem mul_boole