mul_mem_nthRootsFinset — Mathlib

English

If η1 is a root of a1 and η2 is a root of a2, then η1 η2 is a root of a1 a2

Русский

Если η1 — корень a1, а η2 — корень a2, то произведение η1 η2 является корнем a1 a2.

LaTeX

$$$\eta_{1} \in \operatorname{nthRootsFinset}(n, a_{1}) \land \eta_{2} \in \operatorname{nthRootsFinset}(n, a_{2}) \Rightarrow \eta_{1} \eta_{2} \in \operatorname{nthRootsFinset}(n, a_{1} a_{2})$$$

Lean4

theorem mul_mem_nthRootsFinset {η₁ η₂ : R} {a₁ a₂ : R} (hη₁ : η₁ ∈ nthRootsFinset n a₁)
    (hη₂ : η₂ ∈ nthRootsFinset n a₂) : η₁ * η₂ ∈ nthRootsFinset n (a₁ * a₂) := by
  cases n with
  | zero => simp only [nthRootsFinset_zero, notMem_empty] at hη₁
  | succ n =>
    rw [mem_nthRootsFinset n.succ_pos] at hη₁ hη₂ ⊢
    rw [mul_pow, hη₁, hη₂]

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