Theorems · Theorem · functional analysis

smul_mem_closure_star_mul

∀ {R : Type u_1} {A : Type u_2} [inst : Semiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [StarModule R A] [IsScalarTower R A A] [SMulCommClass R A A] {r : R},
  r ∈ AddSubmonoid.closure (Set.range fun s => star s * s) →
    ∀ {a : A},
      a ∈ AddSubmonoid.closure (Set.range fun s => star s * s) →
        r • a ∈ AddSubmonoid.closure (Set.range fun s => star s * s)

Defined in

Mathlib.Algebra.Order.Star.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

SemiringStarRingNonUnitalSemiringStarRingModuleStarModuleIsScalarTowerSMulCommClass