subringClass — Mathlib

English

StarSubalgebra has a SubringClass structure when R is a commutative ring and A is a ring with star.

Русский

StarSubalgebra обладает структурой SubringClass при условии, что R — коммутативное кольцо, а A — кольцо со звездой.

LaTeX

$$$\\text{SubringClass}(\\text{StarSubalgebra }R A, A)$$$

Lean4

instance subringClass {R A} [CommRing R] [StarRing R] [Ring A] [StarRing A] [Algebra R A] [StarModule R A] :
    SubringClass (StarSubalgebra R A) A where neg_mem {s a} ha := show -a ∈ s.toSubalgebra from neg_mem ha

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