hom_ext — Mathlib

English

Another technical lemma used in verifying the equivalence, ensuring compatibility on generators.

Русский

Ещё одна техническая лемма, необходимая для проверки совместимости на порождающих.

LaTeX

$$$\\text{(proof}_{2})$$$

Lean4

/-- Two `R`-algebra morphisms from the quaternions are equal if they agree on `i` and `j`. -/
@[ext]
theorem hom_ext ⦃f g : ℍ[R] →ₐ[R] A⦄ (hi : f (Basis.self R).i = g (Basis.self R).i)
    (hj : f (Basis.self R).j = g (Basis.self R).j) : f = g :=
  QuaternionAlgebra.hom_ext hi hj

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