Theorem ring_hom.ext
Modification history
2022-05-17 13:06
src/algebra/hom/ring.lean
split(algebra/hom/ring): Split off `algebra.ring.basic` (#14144) …
Modified ring_hom.extView on Github →2019-11-07 03:43
src/algebra/ring.lean
feat(extensionality): rename to `ext`; generate `ext` rules for structures (#1645) …
Modified ring_hom.extView on Github →2019-09-24 00:00
src/algebra/ring.lean
refactor(algebra/*): Make `monoid_hom.ext` etc use `∀ x, f x = g x` as an assumption (#1476)
Modified ring_hom.extView on Github →