Theorems · Theorem · field theory

IsAlgebraic.exists_smul_eq_mul

∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] (a : S) {b : S},
  IsAlgebraic R b → b ∈ nonZeroDivisors S → ∃ c d, d ≠ 0 ∧ d • a = b * c

A fraction (a : S) / (b : S) can be reduced to (c : S) / (d : R), if b is algebraic over R.

Defined in

Mathlib.RingTheory.Algebraic.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingRingAlgebra