coe_inj

Mathlib.Algebra.Algebra.Field

URI: https://scilib.ai/kg/mathlib#algebraMap.coe_inj

English

The algebra map from R to A is injective when R is a field and A is a nontrivial R-algebra.

Русский

Алгебраическая карта из R в A инъективна, когда R — поле, а A — ненулёная R-алгебра.

LaTeX

$$$\\operatorname{inj}: \\; \\operatorname{algebraMap}_{R}^{A} : R \\hookrightarrow A.$$$

Lean4

@[norm_cast, simp]
theorem coe_inj {a b : R} : (↑a : A) = ↑b ↔ a = b :=
  (algebraMap R A).injective.eq_iff

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

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

Разделы

Аффилиация

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