instMulZeroClass

Mathlib.Order.Filter.Germ.Basic

URI: https://scilib.ai/kg/mathlib#Filter.Germ.instMulZeroClass

← MathLib Explorer

English

If R is a MulZeroOneClass, then Germ l R is a MulZeroOneClass.

Русский

Если R - MulZeroOneClass, то Germ l R тоже имеет MulZeroOneClass.

LaTeX

$$$ \\mathrm{Germ}(l,R) \\text{ is a MulZeroOneClass}. $$$

Lean4

instance instMulZeroClass [MulZeroClass R] : MulZeroClass (Germ l R) :=
  { zero_mul := Quotient.ind' fun _ => congrArg ofFun <| zero_mul _
    mul_zero := Quotient.ind' fun _ => congrArg ofFun <| mul_zero _ }

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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