Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-11 21:18 ff44ed50

View on Github →

feat({algebra/group_action_hom, data/equiv/mul_add}): add missing inverse defs (#7847)

Estimated changes

Modified src/algebra/group_action_hom.lean

added theorem distrib_mul_action_hom.coe_one

added theorem distrib_mul_action_hom.coe_zero

added def distrib_mul_action_hom.inverse

added theorem distrib_mul_action_hom.one_apply

added theorem distrib_mul_action_hom.to_fun_eq_coe

added theorem distrib_mul_action_hom.zero_apply

added def mul_action_hom.inverse

Modified src/data/equiv/mul_add.lean

added def monoid_hom.inverse