NYLL
Module

MulAction_ncard_orbit_inter_orbit_mul_card.lean

Nyll.AlgebraicCurves.Foundations.Algebra.MulAction_ncard_orbit_inter_orbit_mul_card
7 declarations indexed from sourceView source ↗

Module documentation

Mul Action ncard orbit inter orbit mul card

Imports5
  • Mathlib.GroupTheory.GroupAction.Quotient
  • Mathlib.GroupTheory.Index
  • Mathlib.Data.Set.Card
  • Mathlib.Tactic.Group
  • Mathlib.Tactic.Ring
Imported by2

Declarations

theorem

card_eq_mul_of_card_fiber

L31 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.MulAction_ncard_orbit_inter_orbit_mul_card.S11Orbit.card_eq_mul_of_card_fiber
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.MulAction_ncard_orbit_inter_orbit_mul_card
open MulAction
namespace S11Orbit
Lean source · statement
theorem card_eq_mul_of_card_fiber {α β : Type*} [Finite α] [Finite β] (f : α → β) (c : ℕ)
    (hc : ∀ b, Nat.card {a // f a = b} = c) : Nat.card α = Nat.card β * c
theorem

card_preimage_eq_mul_of_card_fiber

L38 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.MulAction_ncard_orbit_inter_orbit_mul_card.S11Orbit.card_preimage_eq_mul_of_card_fiber
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.MulAction_ncard_orbit_inter_orbit_mul_card
open MulAction
namespace S11Orbit
Lean source · statement
theorem card_preimage_eq_mul_of_card_fiber {α β : Type*} [Finite α] [Finite β] (f : α → β) (c : ℕ)
    (hc : ∀ b, Nat.card {a // f a = b} = c) (t : Set β) :
    Nat.card {a // f a ∈ t} = Nat.card t * c
theorem

card_fiber_smul_eq

L52 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.MulAction_ncard_orbit_inter_orbit_mul_card.S11Orbit.card_fiber_smul_eq
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.MulAction_ncard_orbit_inter_orbit_mul_card
open MulAction
namespace S11Orbit
variable {G : Type*} [Group G] {X : Type*} [MulAction G X]
Lean source · statement
theorem card_fiber_smul_eq (x : X) (g₀ : G) :
    Nat.card {g : G // g • x = g₀ • x} = Nat.card (stabilizer G x)
theorem

card_smul_mem_eq

L60 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.MulAction_ncard_orbit_inter_orbit_mul_card.S11Orbit.card_smul_mem_eq
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.MulAction_ncard_orbit_inter_orbit_mul_card
open MulAction
namespace S11Orbit
variable {G : Type*} [Group G] {X : Type*} [MulAction G X]
Lean source · statement
theorem card_smul_mem_eq [Finite G] (H : Subgroup G) (x : X) (B : Set X) :
    Nat.card {h : H // (h : G) • x ∈ B} = (orbit H x ∩ B).ncard * Nat.card (stabilizer H x)
theorem

card_fiber_psi_eq

L79 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.MulAction_ncard_orbit_inter_orbit_mul_card.S11Orbit.card_fiber_psi_eq
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.MulAction_ncard_orbit_inter_orbit_mul_card
open MulAction
namespace S11Orbit
variable {G : Type*} [Group G] {X : Type*} [MulAction G X]
Lean source · statement
theorem card_fiber_psi_eq (H₁ H₂ : Subgroup G)
    (hprod : ∀ g : G, ∃ h₁ ∈ H₁, ∃ h₂ ∈ H₂, g = h₁ * h₂) (g : G) :
    Nat.card {p : H₁ × H₂ // (p.2 : G)⁻¹ * p.1 = g} = Nat.card (H₁ ⊓ H₂ : Subgroup G)
theorem

ncard_orbit_inter_orbit_mul_card_eq

L106 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.MulAction_ncard_orbit_inter_orbit_mul_card.S11Orbit.ncard_orbit_inter_orbit_mul_card_eq
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.MulAction_ncard_orbit_inter_orbit_mul_card
open MulAction
namespace S11Orbit
variable {G : Type*} [Group G] {X : Type*} [MulAction G X]
Lean source · statement
theorem ncard_orbit_inter_orbit_mul_card_eq [Finite G] [IsPretransitive G X] (H₁ H₂ : Subgroup G)
    (hprod : ∀ g : G, ∃ h₁ ∈ H₁, ∃ h₂ ∈ H₂, g = h₁ * h₂) (x₁ x₂ : X) :
    (orbit H₁ x₁ ∩ orbit H₂ x₂).ncard * Nat.card X = (orbit H₁ x₁).ncard * (orbit H₂ x₂).ncard
theorem

ncard_orbit_inter_orbit_mul_card

L174 ↗
MulAction.ncard_orbit_inter_orbit_mul_card
Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.MulAction_ncard_orbit_inter_orbit_mul_card
open MulAction
Lean source · statement
theorem _root_.MulAction.ncard_orbit_inter_orbit_mul_card {G : Type*} [Group G] {X : Type*}
  [MulAction G X] [Finite G] [MulAction.IsPretransitive G X] (H₁ H₂ : Subgroup G) (hprod : ∀ g : G,
  ∃ h₁ ∈ H₁, ∃ h₂ ∈ H₂, g = h₁ * h₂) (x₁ x₂ : X) :
    (MulAction.orbit H₁ x₁ ∩ MulAction.orbit H₂ x₂).ncard * Nat.card X = (MulAction.orbit H₁
      x₁).ncard * (MulAction.orbit H₂ x₂).ncard

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.