instIsTopologicalSemiring

Mathlib.Topology.Algebra.NonUnitalAlgebra

URI: https://scilib.ai/kg/mathlib#NonUnitalSubalgebra.instIsTopologicalSemiring

English

A non-unital subalgebra S carries a topology making it a topological semiring.

Русский

Ненулевой подалгебра S оснащается топологией, делающей его топологическим полуг Ring.

LaTeX

$$IsTopologicalSemiring s$$

Lean4

instance instIsTopologicalSemiring (s : NonUnitalSubalgebra R A) : IsTopologicalSemiring s :=
  s.toNonUnitalSubsemiring.instIsTopologicalSemiring

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

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

Разделы

Аффилиация

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