Theorems · Theorem · field theory

MulSemiringAction.toAlgAut.congr_simp

∀ (G : Type u_2) (R : Type u_3) (A : Type u_4) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Group G] [inst_4 : MulSemiringAction G A] [inst_5 : SMulCommClass G R A],
  MulSemiringAction.toAlgAut G R A = MulSemiringAction.toAlgAut G R A

Defined in: Mathlib.FieldTheory.Galois.Basic
Cited by: 0 results in Mathlib
Foundations: Depth 31 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommSemiring Semiring Algebra Group MulSemiringAction SMulCommClass

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites9

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
Groupstatement and proof · cited by 6,238
MonoidHomstatement · cited by 3,629
SMulCommClassstatement and proof · cited by 1,927
AlgEquivstatement · cited by 1,681
MulSemiringActionstatement and proof · cited by 423
MulSemiringAction.toAlgAutstatement and proof · cited by 10

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.