Theorems · Theorem · field theory

IsGaloisGroup.finite

∀ (G : Type u_1) [inst : Group G] (R : Type u_5) (B : Type u_6) [inst_1 : CommRing R] [inst_2 : CommRing B]
  [inst_3 : Algebra R B] [Module.Finite R B] [IsDomain B] [inst_6 : MulSemiringAction G B] [IsGaloisGroup G R B],
  Finite G

Defined in: Mathlib.FieldTheory.Galois.IsGaloisGroup
Cited by: 1 results in Mathlib
Foundations: Depth 142 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Group CommRing CommRing Algebra Module.Finite IsDomain MulSemiringAction IsGaloisGroup

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites24

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

CommRingstatement and proof · cited by 17,173
Algebrastatement and proof · cited by 11,388
Groupstatement and proof · cited by 6,238
Algebra.algebraMapproof · cited by 4,706
IsScalarTowerproof · cited by 3,896
Finitestatement · cited by 3,029
IsDomainstatement and proof · cited by 2,196
LT.lt.ne'proof · cited by 1,417
Module.Finitestatement and proof · cited by 1,032
Subringproof · cited by 602
MulSemiringActionstatement and proof · cited by 423
RingHom.toAlgebraproof · cited by 337

Cited by1

Results whose statement or proof uses this declaration.

Ideal.sum_ramification_inertia_eq_cardproof · cited by 1