Theorems · Theorem · field theory

RatFunc.mapRingHom.congr_simp

∀ {R : Type u_3} {S : Type u_4} {F : Type u_5} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : FunLike F (Polynomial R) (Polynomial S)] [inst_3 : RingHomClass F (Polynomial R) (Polynomial S)] (φ φ_1 : F)
  (e_φ : φ = φ_1) (hφ : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial S))),
  RatFunc.mapRingHom φ hφ = RatFunc.mapRingHom φ_1 ⋯

Defined in: Mathlib.FieldTheory.RatFunc.Basic
Cited by: 0 results in Mathlib
Foundations: Depth 113 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing CommRing FunLike RingHomClass

Mathlib docs Source Loogle LeanSearch

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.

CommRingstatement and proof · cited by 17,173
RingHomstatement · cited by 10,189
Polynomialstatement and proof · cited by 5,681
Submonoidstatement · cited by 3,086
FunLikestatement and proof · cited by 2,560
nonZeroDivisorsstatement and proof · cited by 895
RatFuncstatement · cited by 301
RingHomClassstatement and proof · cited by 193
Submonoid.comapstatement and proof · cited by 179
RatFunc.mapRingHomstatement and proof · cited by 2

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.