normalizedGCDMonoid

Mathlib.Algebra.GCDMonoid.PUnit

URI: https://scilib.ai/kg/mathlib#PUnit.normalizedGCDMonoid

Lean4

instance normalizedGCDMonoid : NormalizedGCDMonoid PUnit
    where
  gcd _ _ := unit
  lcm _ _ := unit
  normUnit _ := 1
  normUnit_zero := rfl
  normUnit_mul := by subsingleton
  normUnit_coe_units := by subsingleton
  gcd_dvd_left _ _ := ⟨unit, by subsingleton⟩
  gcd_dvd_right _ _ := ⟨unit, by subsingleton⟩
  dvd_gcd {_ _} _ _ _ := ⟨unit, by subsingleton⟩
  gcd_mul_lcm _ _ := ⟨1, by subsingleton⟩
  lcm_zero_left := by subsingleton
  lcm_zero_right := by subsingleton
  normalize_gcd := by subsingleton
  normalize_lcm := by subsingleton

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

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

Разделы

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

Аффилиация

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