mapEquiv_apply — Mathlib

English

Applying mapEquiv to I yields the same as applying map to I with the underlying algebra equivalence.

Русский

Применение mapEquiv к I эквивалентно применению map к I через соответствующее эквививное отображение.

LaTeX

$$$ (\\mathrm{mapEquiv}\ g)(I) = \\mathrm{map}(\\uparrow g) I $$$

Lean4

@[simp]
theorem mapEquiv_apply (g : P ≃ₐ[R] P') (I : FractionalIdeal S P) : mapEquiv g I = map (↑g) I :=
  rfl

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