exists_smul_eq_mul — Mathlib

English

A variant: if b is algebraic over R and b ≠ 0 in S, then there exists c,d with d a = b c and d ≠ 0.

Русский

Вариант: если b алгебраичен над R и b ≠ 0 в S, то существует c,d такие, что d a = b c и d ≠ 0.

LaTeX

$$$\exists c \in S, \exists d \neq 0,\ d \cdot a = b \cdot c$$$

Lean4

/-- A fraction `(a : S) / (b : S)` can be reduced to `(c : S) / (d : R)`,
if `b` is algebraic over `R`. -/
theorem exists_smul_eq_mul [NoZeroDivisors S] [Algebra.IsAlgebraic R S] (a : S) {b : S} (hb : b ≠ 0) :
    ∃ᵉ (c : S) (d ≠ (0 : R)), d • a = b * c :=
  (isAlgebraic b).exists_smul_eq_mul a (mem_nonZeroDivisors_of_ne_zero hb)

Похожие утверждения