Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-07 09:30 190d4e28

View on Github →

feat(algebra/module/basic): smul_add_hom_one (#7461)

Estimated changes

Modified src/algebra/module/basic.lean

added theorem smul_add_hom_one

Modified src/group_theory/group_action/defs.lean

added theorem const_smul_hom_one