inst — Mathlib

English

A commutative ring R is unramified over itself; i.e., R viewed as an algebra over itself is formally unramified.

Русский

Кольцо R над собой является неразветвленным, то есть формально неразветвлено над самим собой.

LaTeX

$$$\text{FormallyUnramified}(R,R,R)\quad\text{(trivial base)}$$$

Lean4

instance {R : Type*} [CommRing R] : FormallyUnramified R R :=
  by
  rw [iff_comp_injective]
  intro B _ _ _ _ f₁ f₂ _
  exact Subsingleton.elim _ _

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