toUnder_right — Mathlib

English

From an R-algebra map f: A →ₐ[R] B one obtains a morphism in Under R between mkUnder R A and mkUnder R B.

Русский

Из алгебраической гомоморфной карты f: A →ₐ[R] B строится морфизм в Under R между mkUnder R A и mkUnder R B.

LaTeX

$$$f: A \to B \mapsto \text{Under.hom}(\text{mkUnder}(R,A) \to \text{mkUnder}(R,B))$$$

Lean4

@[simp]
theorem toUnder_right {A B : Type u} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (a : A) :
    f.toUnder.right a = f a :=
  rfl

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