instCommRingSubtypeMem

Mathlib.RingTheory.Valuation.ValuationSubring

URI: https://scilib.ai/kg/mathlib#ValuationSubring.instCommRingSubtypeMem

English

Membership in the subring equals membership in the valuation subring instance.

Русский

Членство в подкольце эквивалентно членству в само́й валиационной подобласти.

LaTeX

$$$\forall x, x \in A.toSubring \iff x \in A$$$

Lean4

instance : CommRing A :=
  inferInstanceAs <| CommRing A.toSubring

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru