Theorems · Theorem · ring theory

AlgHomClass.commutes

∀ {F : Type u_1} {R : outParam (Type u_2)} {A : outParam (Type u_3)} {B : outParam (Type u_4)} {inst : CommSemiring R}
  {inst_1 : Semiring A} {inst_2 : Semiring B} {inst_3 : Algebra R A} {inst_4 : Algebra R B} {inst_5 : FunLike F A B}
  [self : AlgHomClass F R A B] (f : F) (r : R), f ((algebraMap R A) r) = (algebraMap R B) r

Defined in

Mathlib.Algebra.Algebra.Hom

Cited by

15 results in Mathlib

Foundations

Depth 16 from the axioms · uses no axioms

Assumes

AlgHomClass