exists_smul_eq_mul — Mathlib

English

If b is algebraic over R and b is a nonzerodivisor of S, then there exist c ∈ S and d ∈ R, d ≠ 0, such that d·a = b·c.

Русский

Если b алгебраичен над R и не нулевой делитель S, то существуют c ∈ S и d ∈ R, d ≠ 0, такие что d·a = b·c.

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 (a : S) {b : S} (hRb : IsAlgebraic R b) (hb : b ∈ S⁰) :
    ∃ᵉ (c : S) (d ≠ (0 : R)), d • a = b * c :=
  have ⟨r, hr, s, h⟩ := hRb.exists_nonzero_dvd hb
  ⟨s * a, r, hr, by rw [Algebra.smul_def, h, mul_assoc]⟩

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