Theorems · Theorem · commutative algebra
AddMonoidHom.ext_int
∀ {A : Type u_5} [inst : AddMonoid A] {f g : ℤ →+ A}, f 1 = g 1 → f = gTwo additive monoid homomorphisms f, g from ℤ to an additive monoid are equal
if f 1 = g 1.
- Defined in
- Mathlib.Data.Int.Cast.Lemmas
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 40 from the axioms · uses propext, Quot.sound
- Assumes
- AddMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
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
- AddMonoidHomstatement and proof · cited by 3,230
- AddMonoidstatement and proof · cited by 2,864
- AddMonoidHom.compproof · cited by 339
- AddMonoidHomClass.toAddMonoidHomproof · cited by 232
- AddMonoidHom.extproof · cited by 149
- DFunLike.ext_iffproof · cited by 102
- Int.ofNatHomproof · cited by 6
- ext_nat'proof · cited by 3
- eq_on_negproof · cited by 1
Cited by7
Results whose statement or proof uses this declaration.
- RingHom.ext_intproof · cited by 25
- AddCommGrpCat.int_hom_extproof · cited by 2
- AddMonoidHom.eq_intCastAddHomproof · cited by 2
- MonoidHom.ext_mintproof · cited by 2
- FreeAbelianGroup.toFinsupp_comp_toFreeAbelianGroupproof · cited by 1
- AddEquiv.ext_intproof · cited by 1
- AddMonoidHom.ext_int_iffproof · cited by 0