toRing — Mathlib

English

A subring S of R inherits a ring structure from R; S with inherited operations forms a ring.

Русский

Подкольцо S ⊆ R наследует структуру кольца от R; с сохраненными операциями S образует кольцо.

LaTeX

$$$Ring\; S$$$

Lean4

/-- A subring of a ring inherits a ring structure -/
instance (priority := 75) toRing : Ring s :=
  fast_instance%Subtype.coe_injective.ring Subtype.val rfl rfl (fun _ _ => rfl) (fun _ _ => rfl) (fun _ => rfl)
      (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ => rfl) fun _ => rfl

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