Theorems · Theorem · group theory
MonoidWithZeroHom.ext
∀ {α : Type u_2} {β : Type u_3} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β] ⦃f g : α →*₀ β⦄,
(∀ (x : α), f x = g x) → f = g- Defined in
- Mathlib.Algebra.GroupWithZero.Hom
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 11 from the axioms · uses Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- MonoidWithZeroHomstatement and proof · cited by 704
- DFunLike.extproof · cited by 240
- MulZeroOneClassstatement and proof · cited by 184
Cited by15
Results whose statement or proof uses this declaration.
- Ring.ordFrac_eq_inverse_comp_valuationproof · cited by 2
- MonoidWithZeroHom.fst_comp_inrproof · cited by 1
- MonoidWithZeroHom.snd_comp_inlproof · cited by 1
- MonoidWithZeroHom.one_compproof · cited by 0
- MonoidWithZeroHom.fst_comp_inlproof · cited by 0
- MonoidWithZeroHom.cancel_leftproof · cited by 0
- MonoidWithZeroHom.cancel_rightproof · cited by 0
- MonoidWithZeroHom.snd_comp_inrproof · cited by 0
- Perfection.mk_comp_teichmuller₀proof · cited by 0
- MonoidWithZeroHom.id_compproof · cited by 0
- MonoidWithZeroHom.mk_coeproof · cited by 0
- WithZero.map'_compproof · cited by 0