norm_mem_spanNorm

Mathlib.RingTheory.Ideal.Norm.RelNorm

URI: https://scilib.ai/kg/mathlib#Ideal.norm_mem_spanNorm

← MathLib Explorer

English

If x ∈ I, then the ordinary norm of x lies in spanNorm R I.

Русский

Если x ∈ I, то нормa Algebra.norm(R, x) принадлежит I.spanNorm.

LaTeX

$$$$\text{If } x\in I,\; \operatorname{norm}(R,x) \in \operatorname{spanNorm}(R,I).$$$$

Lean4

theorem norm_mem_spanNorm [Module.Free R S] {I : Ideal S} (x : S) (hx : x ∈ I) : Algebra.norm R x ∈ I.spanNorm R :=
  by
  refine subset_span ⟨x, hx, ?_⟩
  rw [Algebra.intNorm_eq_norm]

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

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

Разделы

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

Аффилиация

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