English
The NonUnitalStarSubalgebra induces a NonUnitalSubringClass structure, capturing the additive inverses via a compatible negation operation.
Русский
NonUnitalStarSubalgebra индуцирует структуру NonUnitalSubringClass, обеспечивая существование обращения через согласованную операцию отрицания.
LaTeX
$$$\\text{NonUnitalSubringClass }(\\text{NonUnitalStarSubalgebra } R A) A$$$
Lean4
instance (priority := 100) :
CanLift (Set A) (NonUnitalStarSubalgebra R A) (↑)
(fun s ↦
0 ∈ s ∧
(∀ {x y}, x ∈ s → y ∈ s → x + y ∈ s) ∧
(∀ {x y}, x ∈ s → y ∈ s → x * y ∈ s) ∧ (∀ (r : R) {x}, x ∈ s → r • x ∈ s) ∧ ∀ {x}, x ∈ s → star x ∈ s)
where
prf s
h :=
⟨{ carrier := s
zero_mem' := h.1
add_mem' := h.2.1
mul_mem' := h.2.2.1
smul_mem' := h.2.2.2.1
star_mem' := h.2.2.2.2 }, rfl⟩
