mathlib
c50cb7a7 - feat(data/fintype/basic): add decidable_eq_(bundled-hom)_fintype (#7394)

Commit
4 years ago
feat(data/fintype/basic): add decidable_eq_(bundled-hom)_fintype (#7394) Using the proof of `decidable_eq_equiv_fintype` for guidance, this adds equivalent statements about: * `function.embedding` * `zero_hom` * `one_hom` * `add_hom` * `mul_hom` * `add_monoid_hom` * `monoid_hom` * `monoid_with_zero_hom` * `ring_hom` It also fixes a typo that swaps `left` and `right` between two definition names.
Author
Parents
Loading