instCommRingSubtypeMemAddSubgroup

English

If R is a commutative ring, then the self-adjoint elements form a commutative ring under inherited operations.

Русский

Если R — коммутативное кольцо, то самосопряжённые элементы образуют коммутативное кольцо подинкретированными операциями.

LaTeX

$$$\mathrm{CommRing}(\mathrm{selfAdjoint}(R))$$$

Lean4

instance : CommRing (selfAdjoint R) :=
  Function.Injective.commRing _ Subtype.coe_injective (selfAdjoint R).coe_zero val_one (selfAdjoint R).coe_add val_mul
    (selfAdjoint R).coe_neg (selfAdjoint R).coe_sub (by intros; rfl) (by intros; rfl) val_pow (fun _ => rfl) fun _ =>
    rfl

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