le_ofPrime

Mathlib.RingTheory.LocalRing.LocalSubring

URI: https://scilib.ai/kg/mathlib#LocalSubring.le_ofPrime

English

A ≤ (ofPrime A P).toSubring.

Русский

A ≤ (ofPrime A P).toSubring.

LaTeX

$$le_ofPrime: A ≤ (ofPrime A P).toSubring$$

Lean4

theorem le_ofPrime : A ≤ (ofPrime A P).toSubring := by
  intro x hx
  exact ⟨algebraMap A _ ⟨x, hx⟩, by simp⟩

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

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

Разделы

Аффилиация

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