instAddCommMonoidWithOne

Mathlib.RingTheory.PiTensorProduct

URI: https://scilib.ai/kg/mathlib#PiTensorProduct.instAddCommMonoidWithOne

← MathLib Explorer

English

For every natural m, p^m divides (1: PreTilt(O,p)).untiltAux(m) − 1.

Русский

Для каждого натурального m, p^m делит (1:PreTilt(O,p)).untiltAux(m) − 1.

LaTeX

$$$(p : O)^m \mid (1 : PreTilt(O,p)).untiltAux m - 1$$$

Lean4

instance instAddCommMonoidWithOne : AddCommMonoidWithOne (⨂[R] i, A i)
    where
  __ := inferInstanceAs (AddCommMonoid (⨂[R] i, A i))
  __ := instOne

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

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

Разделы

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

Аффилиация

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