Mathlib Map

Theorems · Definition · group theory

Sylow.casesOn

{p : ℕ} →
  {G : Type u_1} →
    [inst : Group G] →
      {motive : Sylow p G → Sort u} →
        (t : Sylow p G) →
          ((toSubgroup : Subgroup G) →
              (isPGroup' : IsPGroup p ↥toSubgroup) →
                (is_maximal' : ∀ {Q : Subgroup G}, IsPGroup p ↥Q → toSubgroup ≤ Q → Q = toSubgroup) →
                  motive { toSubgroup := toSubgroup, isPGroup' := isPGroup', is_maximal' := is_maximal' }) →
            motive t
Defined in
Mathlib.GroupTheory.Sylow
Cited by
1 results in Mathlib
Foundations
Depth 26 from the axioms · uses propext, Quot.sound
Assumes
Group
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Sylow.ext · cited by 3Sylow.extSylow.noConfusion · cited by 0Sylow.noConfusionSylow.noConfusionType · cited by 0Sylow.noConfusionTypeGroup · cited by 6238GroupSubgroup · cited by 3593SubgroupSylow · cited by 103SylowIsPGroup · cited by 96IsPGroupSylow.casesOnCITED BYCITES

Cites4

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

  • Groupstatement and proof · cited by 6,238
  • Subgroupstatement and proof · cited by 3,593
  • Sylowstatement and proof · cited by 103
  • IsPGroupstatement and proof · cited by 96

Cited by3

Results whose statement or proof uses this declaration.