instSubsingletonAlgebra

Mathlib.Algebra.Algebra.ZMod

URI: https://scilib.ai/kg/mathlib#ZMod.instSubsingletonAlgebra

English

Characterization of idempotence in the unitization via the underlying element.

Русский

Характеризация идемпотентности в единичизации через базовый элемент.

LaTeX

$$Iff (IsIdempotentElem (Unitization.inr a)) (IsIdempotentElem a)$$

Lean4

instance (p : ℕ) : Subsingleton (Algebra (ZMod p) R) :=
  ⟨fun _ _ => Algebra.algebra_ext _ _ <| RingHom.congr_fun <| Subsingleton.elim _ _⟩

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

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

Разделы

Аффилиация

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