Theorems · Theorem · commutative algebra

Algebra.pow_smul_mem_of_smul_subset_of_mem_adjoin

∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  [inst_3 : CommSemiring B] [inst_4 : Algebra R B] [inst_5 : Algebra A B] [IsScalarTower R A B] (r : A) (s : Set B)
  (B' : Subalgebra R B),
  r • s ⊆ ↑B' → ∀ {x : B}, x ∈ Algebra.adjoin R s → (algebraMap A B) r ∈ B' → ∃ n₀, ∀ n ≥ n₀, r ^ n • x ∈ B'

Defined in

Mathlib.RingTheory.Adjoin.Basic

Cited by

2 results in Mathlib

Foundations

Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringCommSemiringAlgebraCommSemiringAlgebraAlgebraIsScalarTower