Theorems · Theorem · commutative algebra
DualNumber.ringHom_ext
∀ {R : Type u_1} [inst : CommSemiring R] {R' : Type u_5} [inst_1 : CommSemiring R'] {f g : DualNumber R →+* R'},
f.comp (algebraMap R (DualNumber R)) = g.comp (algebraMap R (DualNumber R)) →
f DualNumber.eps = g DualNumber.eps → f = gA ring morphism R[ε] →+* R' is determined by its restriction
on R and its value on ε.
- Defined in
- Mathlib.Algebra.DualNumber
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 40 from the axioms · uses propext, Quot.sound
- Assumes
- CommSemiringCommSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
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
- Algebraproof · cited by 11,388
- CommSemiringstatement and proof · cited by 10,911
- RingHomstatement and proof · cited by 10,189
- Algebra.algebraMapstatement and proof · cited by 4,706
- AlgHomproof · cited by 3,236
- MulOppositestatement · cited by 1,135
- RingHom.compstatement and proof · cited by 899
- AlgHom.toRingHomproof · cited by 490
- DFunLike.congr_funproof · cited by 288
- DualNumberstatement and proof · cited by 52
- DualNumber.epsstatement and proof · cited by 30
Cited by1
Results whose statement or proof uses this declaration.
- DualNumber.ringHom_ext_iffproof · cited by 0