mapₐ_apply — Mathlib

English

The value of mapₐ on an element agrees with the previously defined map on the same input.

Русский

Значение mapₐ на элементе совпадает с ранее заданным отображением на том же входе.

LaTeX

$$$\mathrm{map}_a(I,J,hf,x) = \mathrm{map}(I,J,\mathrm{algebraMap},hf,x).$$$

Lean4

@[simp]
theorem mapₐ_apply (I : Ideal R) [I.IsPrime] (J : Ideal A) [J.IsPrime] (hf : I = J.comap (algebraMap R A)) (x) :
    Ideal.ResidueField.mapₐ I J hf x = Ideal.ResidueField.map I J _ hf x :=
  rfl

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