Commit 2023-03-19 01:36 05101c3d

View on Github →

feat(algebra/group/commute): div lemmas (#18607) commute analogs of existing lemmas. Also normalise lemma names about commute and nat.cast/int.cast, following existing int.cast lemmas.

Estimated changes

Modified src/algebra/field/basic.lean

Modified src/algebra/group/commute.lean

deleted theorem commute.inv_inv

Modified src/algebra/group_power/lemmas.lean

modified theorem commute.cast_int_left

modified theorem commute.cast_int_right

modified theorem commute.cast_nat_mul_self

modified theorem commute.self_cast_nat_mul

modified theorem commute.self_cast_nat_mul_cast_nat_mul