Module

Subgroup_exists_eq_mul_of_index_inf_eq.lean

Nyll.AlgebraicCurves.Foundations.Algebra.Subgroup_exists_eq_mul_of_index_inf_eq

3 declarations indexed from sourceView source ↗

Module documentation

Subgroup exists eq mul of index inf eq

Imports4

Mathlib.GroupTheory.GroupAction.Quotient
Mathlib.GroupTheory.Index
Mathlib.Data.Set.Card
Mathlib.Tactic.Group

Imported by2

theorem

stabilizer_mk_one_eq

L32 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Subgroup_exists_eq_mul_of_index_inf_eq.S11Orbit2.stabilizer_mk_one_eq

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Subgroup_exists_eq_mul_of_index_inf_eq
open MulAction
namespace S11Orbit2
variable {G : Type*} [Group G]

Lean source · statement

theorem stabilizer_mk_one_eq (H₁ H₂ : Subgroup G) :
    stabilizer H₂ ((1 : G) : G ⧸ H₁) = H₁.subgroupOf H₂

theorem

exists_eq_mul_of_index_inf_eq

L39 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Subgroup_exists_eq_mul_of_index_inf_eq.S11Orbit2.exists_eq_mul_of_index_inf_eq

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Subgroup_exists_eq_mul_of_index_inf_eq
open MulAction
namespace S11Orbit2
variable {G : Type*} [Group G]

Lean source · statement

theorem exists_eq_mul_of_index_inf_eq [Finite G] (H₁ H₂ : Subgroup G)
    (h : (H₁ ⊓ H₂).index = H₁.index * H₂.index) (g : G) :
    ∃ h₁ ∈ H₁, ∃ h₂ ∈ H₂, g = h₁ * h₂

theorem

exists_eq_mul_of_index_inf_eq

L62 ↗

Subgroup.exists_eq_mul_of_index_inf_eq

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Subgroup_exists_eq_mul_of_index_inf_eq
open MulAction

Lean source · statement

theorem _root_.Subgroup.exists_eq_mul_of_index_inf_eq {G : Type*} [Group G] [Finite G] (H₁ H₂ :
  Subgroup G) (h : (H₁ ⊓ H₂).index = H₁.index * H₂.index) (g : G) :
    ∃ h₁ ∈ H₁, ∃ h₂ ∈ H₂, g = h₁ * h₂

Module documentation

Subgroup exists eq mul of index inf eq

Declarations

stabilizer_mk_one_eq

exists_eq_mul_of_index_inf_eq

exists_eq_mul_of_index_inf_eq