mathlib3
8f391aa5 - chore(algebra/module/submodule): switch `subtype_eq_val` to `coe_subtype` (#11210)

Commit
3 years ago
chore(algebra/module/submodule): switch `subtype_eq_val` to `coe_subtype` (#11210) Change the name and form of a lemma, from ```lean lemma subtype_eq_val : ((submodule.subtype p) : p → M) = subtype.val := rfl ``` to ```lean lemma coe_subtype : ((submodule.subtype p) : p → M) = coe := rfl ``` The latter is the simp-normal form so I claim it should be preferred.
Author
Parents
Loading