le_one_toAddSubmonoid

Mathlib.Algebra.Algebra.Operations

URI: https://scilib.ai/kg/mathlib#Submodule.le_one_toAddSubmonoid

← MathLib Explorer

English

The order relation on Submodule is captured by: 1 ≤ P iff 1 ∈ P.

Русский

Порядок на Submodule выражается как: 1 ≤ P тогда и только тогда, когда 1 ∈ P.

LaTeX

$$$(1 : Submodule R A) \\le P \\iff (1 : A) \\in P$$$

Lean4

theorem le_one_toAddSubmonoid : 1 ≤ (1 : Submodule R A).toAddSubmonoid :=
  by
  rintro x ⟨n, rfl⟩
  exact ⟨n, show (n : R) • (1 : A) = n by rw [Nat.cast_smul_eq_nsmul, nsmul_one]⟩

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

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

Разделы

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

Аффилиация

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