Theorems · Theorem · field theory

RatFunc.eval_mul

∀ {K : Type u} [inst : Field K] {L : Type u} [inst_1 : Field L] (f : K →+* L) (a : L) {x y : RatFunc K},
  Polynomial.eval₂ f a x.denom ≠ 0 →
    Polynomial.eval₂ f a y.denom ≠ 0 → RatFunc.eval f a (x * y) = RatFunc.eval f a x * RatFunc.eval f a y

eval is a multiplicative homomorphism except when a denominator evaluates to 0. Counterexample: eval _ 0 X * eval _ 0 (1/X) = 0 ≠ 1 = eval _ 0 1 = eval _ 0 (X * 1/X). See also RatFunc.eval₂_denom_ne_zero to make the hypotheses simpler but less general.

Defined in

Mathlib.FieldTheory.RatFunc.AsPolynomial

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldField