Theorems · Theorem · field theory

RatFunc.liftOn.congr_simp

∀ {K : Type u_1} [inst : CommRing K] {P : Sort u_2} (x x_1 : RatFunc K),
  x = x_1 →
    ∀ (f f_1 : Polynomial K → Polynomial K → P) (e_f : f = f_1)
      (H :
        ∀ {p q p' q' : Polynomial K},
          q ∈ nonZeroDivisors (Polynomial K) → q' ∈ nonZeroDivisors (Polynomial K) → q' * p = q * p' → f p q = f p' q'),
      x.liftOn f H = x_1.liftOn f_1 ⋯

Defined in

Mathlib.FieldTheory.RatFunc.Defs

Cited by

1 results in Mathlib

Foundations

Depth 99 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRing