Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-04 22:36 ce0e0583

View on Github →

feat(data/equiv/mul_add): add lemmas about multiplication and addition on a group being bijective and finite cancel_monoid_with_zeros (#10046)

Estimated changes

Modified src/data/equiv/mul_add.lean

added theorem group.mul_left_bijective

added theorem group.mul_right_bijective

added theorem mul_left_bijective₀

added theorem mul_right_bijective₀

added theorem units.mul_left_bijective

added theorem units.mul_right_bijective

Modified src/ring_theory/integral_domain.lean

added def group_with_zero_of_fintype

added theorem mul_left_bijective_of_fintype₀

deleted theorem mul_left_bijective₀

added theorem mul_right_bijective_of_fintype₀

deleted theorem mul_right_bijective₀