Theorems · Theorem · number theory

MulSemiringAction.toAlgHom.congr_simp

∀ {M : Type u_1} (R : Type u_3) (A : Type u_4) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Monoid M] [inst_4 : MulSemiringAction M A] [inst_5 : SMulCommClass M R A] (m m_1 : M),
  m = m_1 → MulSemiringAction.toAlgHom R A m = MulSemiringAction.toAlgHom R A m_1

Defined in: Mathlib.RingTheory.Frobenius
Cited by: 0 results in Mathlib
Foundations: Depth 22 from the axioms · uses no axioms
Assumes: CommSemiring Semiring Algebra Monoid MulSemiringAction SMulCommClass

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Semiringstatement and proof · cited by 13,802
Algebrastatement and proof · cited by 11,388
CommSemiringstatement and proof · cited by 10,911
Monoidstatement and proof · cited by 3,887
AlgHomstatement · cited by 3,236
SMulCommClassstatement and proof · cited by 1,927
MulSemiringActionstatement and proof · cited by 423
MulSemiringAction.toAlgHomstatement and proof · cited by 10

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.