isIntegral_algEquiv — Mathlib

English

For an algebra equivalence f: A ≃ₐ[R] B, IsIntegral R (f x) iff IsIntegral R x.

Русский

Для алгебра эквивалентности f: A ≃ₐ[R] B выполняется IsIntegral R (f(x)) iff IsIntegral R x.

LaTeX

$$$\\text{IsIntegral}_R(f(x)) \\iff \\text{IsIntegral}_R(x)$$$

Lean4

@[simp]
theorem isIntegral_algEquiv {A B : Type*} [Ring A] [Ring B] [Algebra R A] [Algebra R B] (f : A ≃ₐ[R] B) {x : A} :
    IsIntegral R (f x) ↔ IsIntegral R x :=
  ⟨fun h ↦ by simpa using h.map f.symm, IsIntegral.map f⟩

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