Theorems · Theorem · commutative algebra

DualNumber.ringHom_ext_iff

∀ {R : Type u_1} [inst : CommSemiring R] {R' : Type u_5} [inst_1 : CommSemiring R'] {f g : DualNumber R →+* R'},
  f = g ↔
    f.comp (algebraMap R (DualNumber R)) = g.comp (algebraMap R (DualNumber R)) ∧ f DualNumber.eps = g DualNumber.eps

Defined in: Mathlib.Algebra.DualNumber
Cited by: 0 results in Mathlib
Foundations: Depth 41 from the axioms · uses propext, Quot.sound
Assumes: CommSemiring CommSemiring

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites9

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
CommSemiringstatement and proof · cited by 10,911
RingHomstatement and proof · cited by 10,189
Algebra.algebraMapstatement and proof · cited by 4,706
MulOppositestatement · cited by 1,135
RingHom.compstatement and proof · cited by 899
DualNumberstatement and proof · cited by 52
DualNumber.epsstatement and proof · cited by 30
DualNumber.ringHom_extproof · cited by 1

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.