isoBaseOfIsPrincipal_apply — Mathlib

English

Under the isPrincipal isomorphism, the image of x is x times the generator of I.

Русский

Предел изоморфизма isPrincipal отображает x в x, умноженное на генератор I.

LaTeX

$$$(Ideal.isoBaseOfIsPrincipal\ hI)\ x = x \cdot \mathrm{IsPrincipal.generator } I$$$

Lean4

@[simp]
theorem isoBaseOfIsPrincipal_apply {I : Ideal R} [hprinc : I.IsPrincipal] (hI : I ≠ ⊥) (x : R) :
    (Ideal.isoBaseOfIsPrincipal hI) x = x * IsPrincipal.generator I :=
  rfl

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