Theorems · Theorem · commutative algebra

IsGaloisGroup.faithful

∀ {G : Type u_1} (A : Type u_2) {B : Type u_4} {inst : Group G} {inst_1 : CommSemiring A} {inst_2 : Semiring B}
  {inst_3 : Algebra A B} {inst_4 : MulSemiringAction G B} [self : IsGaloisGroup G A B], FaithfulSMul G B

Defined in

Mathlib.RingTheory.IsGaloisGroup.Defs

Cited by

6 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms

Assumes

IsGaloisGroup