radical_prod_dvd — Mathlib

English

For a finite set s and function f, radical of the product over s divides the product of radicals.

Русский

Для множества s и функции f радикал произведения по s делит произведение радикалов.

LaTeX

$$$\operatorname{radical}\left( \prod_{i\in s} f(i) \right) \mid \prod_{i\in s} \operatorname{radical}(f(i))$$$

Lean4

theorem radical_prod_dvd {ι : Type*} {s : Finset ι} {f : ι → M} : radical (∏ i ∈ s, f i) ∣ ∏ i ∈ s, radical (f i) := by
  induction s using Finset.cons_induction with
  | empty => simp
  | cons i s h ih =>
    simp only [Finset.prod_cons]
    exact radical_mul_dvd.trans (mul_dvd_mul_left _ ih)

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