of_mem_closure' — Mathlib

English

For x in A and positive n, IsIntegral R (x^n) iff IsIntegral R x.

Русский

Для x в A и положительного n выполняется IsIntegral R (x^n) ⇔ IsIntegral R x.

LaTeX

$$$0 < n \Rightarrow (IsIntegral R (x^n) \iff IsIntegral R x)$$$

Lean4

/-- Generalization of `IsIntegral.of_mem_closure` bootstrapped up from that lemma -/
theorem of_mem_closure' (G : Set A) (hG : ∀ x ∈ G, IsIntegral R x) : ∀ x ∈ Subring.closure G, IsIntegral R x :=
  fun _ hx ↦
  Subring.closure_induction hG isIntegral_zero isIntegral_one (fun _ _ _ _ ↦ IsIntegral.add) (fun _ _ ↦ IsIntegral.neg)
    (fun _ _ _ _ ↦ IsIntegral.mul) hx

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