Built with Alectryon. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
Hover-Settings: Show types: Show goals:
import Mathlib.Algebra.Group.Defs
import Mathlib.GroupTheory.SpecificGroups.Alternating
import Mathlib.GroupTheory.SpecificGroups.Cyclic
import Mathlib.GroupTheory.SpecificGroups.Dihedral
import Mathlib.GroupTheory.SpecificGroups.KleinFour
import Mathlib.GroupTheory.SpecificGroups.Quaternion
-- import Mathlib.GroupTheory.Subgroup.Actions
-- import Mathlib.GroupTheory.Subgroup.Basic
-- import Mathlib.GroupTheory.Subgroup.Finite
-- import Mathlib.GroupTheory.Subgroup.MulOpposite
-- import Mathlib.GroupTheory.Subgroup.Pointwise
-- import Mathlib.GroupTheory.Subgroup.Saturated
-- import Mathlib.GroupTheory.Subgroup.Simple
-- import Mathlib.GroupTheory.Subgroup.ZPowers
import Mathlib.RepresentationTheory.Basic
import Mathlib.RepresentationTheory.Action.Basic
import Mathlib.CategoryTheory.Endomorphism
import Mathlib.GroupTheory.GroupAction.Basic
import Mathlib.GroupTheory.GroupAction.DomAct.Basic
import Mathlib.Algebra.DirectSum.Algebra
import Mathlib.LinearAlgebra.Matrix.Basis
import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
import Mathlib.Data.Matrix.Invertible
import Mathlib.LinearAlgebra.Eigenspace.Basic
import Mathlib.GroupTheory.Index
import Mathlib.LinearAlgebra.Eigenspace.Triangularizable
import Mathlib.LinearAlgebra.Matrix.Spectrum
import Mathlib.GroupTheory.FreeGroup.IsFreeGroup
-- import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup
import Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
import Mathlib.GroupTheory.SemidirectProduct
import Mathlib.Logic.Equiv.Defs
-- import Mathlib.Data.ZMod.Module
import Mathlib.GroupTheory.PresentedGroup
-- import Mathlib.GroupTheory.Commutator
import Mathlib.GroupTheory.Coprod.Basic
import Mathlib.Tactic

-- Inspired by Finite symmetric groups in Physics
-- Following Representations and Characters of Groups


Representation.trivial.{u_1, u_2, u_3} (k : Type u_1) {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G]
  [AddCommMonoid V] [Module k V] : Representation k G V
 
Representation.trivial: (k : Type u_1) →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : CommSemiring k] →
        [inst_1 : Monoid G] → [inst_2 : AddCommMonoid V] → [inst_3 : Module k V] → Representation k G V
Representation.trivial


Module.End.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Type v
 
Module.End: (R : Type u) → (M : Type v) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst : Module R M] → Type v
Module.End


DistribMulAction.toModuleEnd.{u_1, u_4, u_5} (R : Type u_1) {S : Type u_4} (M : Type u_5) [Semiring R] [AddCommMonoid M]
  [Module R M] [Monoid S] [DistribMulAction S M] [SMulCommClass S R M] : S →* Module.End R M
 
DistribMulAction.toModuleEnd: (R : Type u_1) →
  {S : Type u_4} →
    (M : Type u_5) →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : Monoid S] → [inst_4 : DistribMulAction S M] → [inst_5 : SMulCommClass S R M] → S →* Module.End R M
DistribMulAction.toModuleEnd


CategoryTheory.End.{v, u} {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] (X : C) : Type v
 
CategoryTheory.End: {C : Type u} → [inst : CategoryTheory.CategoryStruct.{v, u} C] → C → Type v
CategoryTheory.End


CategoryTheory.Aut.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : Type v
 
CategoryTheory.Aut: {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → C → Type v
CategoryTheory.Aut


Action.ρAut.{u} {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : Grp} (A : Action V (MonCat.of ↑G)) :
  G ⟶ Grp.of (CategoryTheory.Aut A.V)
 
Action.ρAut: {V : Type (u + 1)} →
  [inst : CategoryTheory.LargeCategory V] →
    {G : Grp} → (A : Action V (MonCat.of ↑G)) → G ⟶ Grp.of (CategoryTheory.Aut A.V)
Action.ρAut


Fact (p : Prop) : Prop
 
Fact: Prop → Prop
Fact


IsCyclic.exists_generator.{u} {α : Type u} [Group α] [IsCyclic α] : ∃ g, ∀ (x : α), x ∈ Subgroup.zpowers g
 
IsCyclic.exists_generator: ∀ {α : Type u} [inst : Group α] [inst_1 : IsCyclic α], ∃ g, ∀ (x : α), x ∈ Subgroup.zpowers g
IsCyclic.exists_generator


isCyclic_of_prime_card.{u} {α : Type u} [Group α] [Fintype α] {p : ℕ} [hp : Fact (Nat.Prime p)]
  (h : Fintype.card α = p) : IsCyclic α
 
isCyclic_of_prime_card: ∀ {α : Type u} [inst : Group α] [inst_1 : Fintype α] {p : ℕ} [hp : Fact (Nat.Prime p)], Fintype.card α = p → IsCyclic α
isCyclic_of_prime_card

variable (
p: ℕ
p : 
ℕ: Type
ℕ) [
Fact: Prop → Prop
Fact 
p: ℕ
p.
Prime: ℕ → Prop
Prime] (
F: Type uF
F : 
Type uF: Type (uF + 1)
Type uF) [
Field: Type uF → Type uF
Field 
F: Type uF
F] (
ι: Type uι
ι : 
Type uι: Type (uι + 1)
Type uι) [
Finite: Type uι → Prop
Finite 
ι: Type uι
ι] [
LT: Type uι → Type uι
LT 
ι: Type uι
ι] (
R: Type uR
R : 
Type uR: Type (uR + 1)
Type uR) [
Ring: Type uR → Type uR
Ring 
R: Type uR
R] -- (fp : ι → F)

-- a list of indices, sorted
abbrev 
Model.Index: (ι : Type uι) → [inst : LT ι] → Type uι
Model.Index := {
l: List ι
l : 
List: Type uι → Type uι
List 
ι: Type uι
ι // 
l: List ι
l.
Sorted: {α : Type uι} → (α → α → Prop) → List α → Prop
Sorted 
(· < ·): ι → ι → Prop
(· < ·) }

def 
fp: Type (max uι uF)
fp := 
Model.Index: (ι : Type uι) → [inst : LT ι] → Type uι
Model.Index 
ι: Type uι
ι →₀ 
F: Type uF
F

def 
ee: fp F ι → fp F ι
ee (
g: fp F ι
g : 
fp: (F : Type uF) → [inst : Field F] → (ι : Type uι) → [inst : LT ι] → Type (max uι uF)
fp 
F: Type uF
F 
ι: Type uι
ι) : 
fp: (F : Type uF) → [inst : Field F] → (ι : Type uι) → [inst : LT ι] → Type (max uι uF)
fp 
F: Type uF
F 
ι: Type uι
ι := 
g: fp F ι
g


Fin p : Type
 
Fin: ℕ → Type
Fin 
p: ℕ
p

-- def Fp : Fin p → F := sorry

-- https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Action.20of.20permutations.20on.20functions.2E


Warning: declaration uses 'sorry'
 : 
MulAction: (α : Type u_1) → Type u_1 → [inst : Monoid α] → Type u_1
MulAction (
Equiv.Perm: Type u_1 → Type (max 0 u_1)
Equiv.Perm 
β: Type u_1
β)ᵐᵒᵖ 
β: Type u_1
β := 
sorry: MulAction (Equiv.Perm β)ᵐᵒᵖ β
sorry

variable (
α: Type u_1
α 
β: Type u_2
β : 
Type*: Type (u_2 + 1)
Type*) in

DomMulAct.instMulActionForall
 -- works


-- variable (α β : Type*) in
-- #synth MulAction ((Equiv.Perm α)ᵈᵐᵃ)ᵐᵒᵖ (α → β) -- fails


import Mathlib.Algebra.Field.Defs
import Mathlib.Data.Finsupp.Defs
import Mathlib.GroupTheory.Perm.Basic
Warning: '#minimize_imports' is deprecated: please use '#min_imports'



Group.{u} (G : Type u) : Type u
 
Group: Type u → Type u
Group


Semigroup.mul_assoc.{u} {G : Type u} [self : Semigroup G] (a b c : G) : a * b * c = a * (b * c)
 
Semigroup.mul_assoc: ∀ {G : Type u} [self : Semigroup G] (a b c : G), a * b * c = a * (b * c)
Semigroup.mul_assoc


MulOneClass.one_mul.{u} {M : Type u} [self : MulOneClass M] (a : M) : 1 * a = a
 
MulOneClass.one_mul: ∀ {M : Type u} [self : MulOneClass M] (a : M), 1 * a = a
MulOneClass.one_mul


MulOneClass.mul_one.{u} {M : Type u} [self : MulOneClass M] (a : M) : a * 1 = a
 
MulOneClass.mul_one: ∀ {M : Type u} [self : MulOneClass M] (a : M), a * 1 = a
MulOneClass.mul_one


mul_left_inv.{u_1} {G : Type u_1} [Group G] (a : G) : a⁻¹ * a = 1
 
mul_left_inv: ∀ {G : Type u_1} [inst : Group G] (a : G), a⁻¹ * a = 1
mul_left_inv


Subgroup.{u_5} (G : Type u_5) [Group G] : Type u_5
 
Subgroup: (G : Type u_5) → [inst : Group G] → Type u_5
Subgroup

variable {
G: Type uG
G 
H: Type uG
H : 
Type uG: Type (uG + 1)
Type uG} [
Group: Type uG → Type uG
Group 
G: Type uG
G] [
Group: Type uG → Type uG
Group 
H: Type uG
H] (
K: Subgroup G
K 
L: Subgroup G
L : 
Subgroup: (G : Type uG) → [inst : Group G] → Type uG
Subgroup 
G: Type uG
G)


Subgroup G : Type uG
 
Subgroup: (G : Type uG) → [inst : Group G] → Type uG
Subgroup 
G: Type uG
G


G × H : Type uG
 
G: Type uG
G × 
H: Type uG
H


Prod.instGroup.{u_1, u_2} {G : Type u_1} {H : Type u_2} [Group G] [Group H] : Group (G × H)
 
Prod.instGroup: {G : Type u_1} → {H : Type u_2} → [inst : Group G] → [inst : Group H] → Group (G × H)
Prod.instGroup


Group.FG.{u_3} (G : Type u_3) [Group G] : Prop
 
Group.FG: (G : Type u_3) → [inst : Group G] → Prop
Group.FG


MulHom.{u_10, u_11} (M : Type u_10) (N : Type u_11) [Mul M] [Mul N] : Type (max u_10 u_11)
 
MulHom: (M : Type u_10) → (N : Type u_11) → [inst : Mul M] → [inst : Mul N] → Type (max u_10 u_11)
MulHom


MonoidHom.{u_10, u_11} (M : Type u_10) (N : Type u_11) [MulOneClass M] [MulOneClass N] : Type (max u_10 u_11)
 
MonoidHom: (M : Type u_10) → (N : Type u_11) → [inst : MulOneClass M] → [inst : MulOneClass N] → Type (max u_10 u_11)
MonoidHom


Action.Hom.{u} {V : Type (u + 1)} [CategoryTheory.LargeCategory V] {G : MonCat} (M N : Action V G) : Type u
 
Action.Hom: {V : Type (u + 1)} → [inst : CategoryTheory.LargeCategory V] → {G : MonCat} → Action V G → Action V G → Type u
Action.Hom


Representation.asGroupHom.{u_1, u_2, u_3} {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G]
  [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : G →* (V →ₗ[k] V)ˣ
 
Representation.asGroupHom: {k : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : CommSemiring k] →
        [inst_1 : Group G] →
          [inst_2 : AddCommMonoid V] → [inst_3 : Module k V] → Representation k G V → G →* (V →ₗ[k] V)ˣ
Representation.asGroupHom


Subgroup.Normal.{u_1} {G : Type u_1} [Group G] (H : Subgroup G) : Prop
 
Subgroup.Normal: {G : Type u_1} → [inst : Group G] → Subgroup G → Prop
Subgroup.Normal


Subgroup.index.{u_1} {G : Type u_1} [Group G] (H : Subgroup G) : ℕ
 
Subgroup.index: {G : Type u_1} → [inst : Group G] → Subgroup G → ℕ
Subgroup.index


G ⧸ K : Type uG
 
HasQuotient.Quotient: (A : outParam (Type uG)) → {B : Type uG} → [inst : HasQuotient A B] → B → Type uG
HasQuotient.Quotient 
G: Type uG
G 
K: Subgroup G
K

/-
failed to synthesize instance
  HDiv (Type uG) (Subgroup G) ?m.4221
-/
-- #check G / K


IsSimpleGroup.{u_1} (G : Type u_1) [Group G] : Prop
 
IsSimpleGroup: (G : Type u_1) → [inst : Group G] → Prop
IsSimpleGroup


QuotientGroup.instHasQuotientSubgroup.{u_1} {α : Type u_1} [Group α] : HasQuotient α (Subgroup α)
 
QuotientGroup.instHasQuotientSubgroup: {α : Type u_1} → [inst : Group α] → HasQuotient α (Subgroup α)
QuotientGroup.instHasQuotientSubgroup


QuotientGroup.Quotient.group.{u} {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] : Group (G ⧸ N)
 
QuotientGroup.Quotient.group: {G : Type u} → [inst : Group G] → (N : Subgroup G) → [nN : N.Normal] → Group (G ⧸ N)
QuotientGroup.Quotient.group


LinearMap.ker.{u_1, u_2, u_5, u_7, u_11} {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [Semiring R]
  [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_11}
  [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] (f : F) : Submodule R M
 
LinearMap.ker: {R : Type u_1} →
  {R₂ : Type u_2} →
    {M : Type u_5} →
      {M₂ : Type u_7} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R₂ M₂] →
                    {τ₁₂ : R →+* R₂} →
                      {F : Type u_11} →
                        [inst_6 : FunLike F M M₂] → [inst_7 : SemilinearMapClass F τ₁₂ M M₂] → F → Submodule R M
LinearMap.ker


Set.preimage_kernImage.{u_1, u_2} {α : Type u_1} {β : Type u_2} {f : α → β} :
  GaloisConnection (Set.preimage f) (Set.kernImage f)
 
Set.preimage_kernImage: ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, GaloisConnection (Set.preimage f) (Set.kernImage f)
Set.preimage_kernImage


Setoid.ker.{u_1, u_2} {α : Type u_1} {β : Type u_2} (f : α → β) : Setoid α
 
Setoid.ker: {α : Type u_1} → {β : Type u_2} → (α → β) → Setoid α
Setoid.ker


Filter.ker.{u_1} {α : Type u_1} (f : Filter α) : Set α
 
Filter.ker: {α : Type u_1} → Filter α → Set α
Filter.ker


MonoidHom.ker.{u_1, u_7} {G : Type u_1} [Group G] {M : Type u_7} [MulOneClass M] (f : G →* M) : Subgroup G
 
MonoidHom.ker: {G : Type u_1} → [inst : Group G] → {M : Type u_7} → [inst_1 : MulOneClass M] → (G →* M) → Subgroup G
MonoidHom.ker


RingHom.ker.{u, v, u_1} {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S]
  [rcf : RingHomClass F R S] (f : F) : Ideal R
 
RingHom.ker: {R : Type u} →
  {S : Type v} →
    {F : Type u_1} →
      [inst : Semiring R] → [inst_1 : Semiring S] → [inst_2 : FunLike F R S] → [rcf : RingHomClass F R S] → F → Ideal R
RingHom.ker


MonoidHom.range.{u_1, u_5} {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) : Subgroup N
 
MonoidHom.range: {G : Type u_1} → [inst : Group G] → {N : Type u_5} → [inst_1 : Group N] → (G →* N) → Subgroup N
MonoidHom.range


QuotientGroup.quotientKerEquivRange.{u, v} {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) :
  G ⧸ φ.ker ≃* ↥φ.range
 
QuotientGroup.quotientKerEquivRange: {G : Type u} → [inst : Group G] → {H : Type v} → [inst_1 : Group H] → (φ : G →* H) → G ⧸ φ.ker ≃* ↥φ.range
QuotientGroup.quotientKerEquivRange


QuotientGroup.quotientInfEquivProdNormalQuotient.{u} {G : Type u} [Group G] (H N : Subgroup G) [N.Normal] :
  ↥H ⧸ N.subgroupOf H ≃* ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N)
 
QuotientGroup.quotientInfEquivProdNormalQuotient: {G : Type u} →
  [inst : Group G] → (H N : Subgroup G) → [inst_1 : N.Normal] → ↥H ⧸ N.subgroupOf H ≃* ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N)
QuotientGroup.quotientInfEquivProdNormalQuotient


QuotientGroup.quotientQuotientEquivQuotient.{u} {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G)
  [nM : M.Normal] (h : N ≤ M) : (G ⧸ N) ⧸ Subgroup.map (QuotientGroup.mk' N) M ≃* G ⧸ M
 
QuotientGroup.quotientQuotientEquivQuotient: {G : Type u} →
  [inst : Group G] →
    (N : Subgroup G) →
      [nN : N.Normal] →
        (M : Subgroup G) → [nM : M.Normal] → N ≤ M → (G ⧸ N) ⧸ Subgroup.map (QuotientGroup.mk' N) M ≃* G ⧸ M
QuotientGroup.quotientQuotientEquivQuotient


Basis.{u_1, u_3, u_6} (ι : Type u_1) (R : Type u_3) (M : Type u_6) [Semiring R] [AddCommMonoid M] [Module R M] :
  Type (max (max u_1 u_3) u_6)
 
Basis: Type u_1 →
  (R : Type u_3) →
    (M : Type u_6) →
      [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst : Module R M] → Type (max (max u_1 u_3) u_6)
Basis


Module.Finite.of_basis.{u_1, u_2, u_3} {R : Type u_1} {M : Type u_2} {ι : Type u_3} [Semiring R] [AddCommMonoid M]
  [Module R M] [Finite ι] (b : Basis ι R M) : Module.Finite R M
 
Module.Finite.of_basis: ∀ {R : Type u_1} {M : Type u_2} {ι : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Finite ι], Basis ι R M → Module.Finite R M
Module.Finite.of_basis


Module.Free.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Prop
 
Module.Free: (R : Type u) → (M : Type v) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst : Module R M] → Prop
Module.Free


Module.Finite.finite_basis.{u_6, u_7, u_8} {R : Type u_6} {M : Type u_7} [Semiring R] [Nontrivial R] [AddCommGroup M]
  [Module R M] {ι : Type u_8} [Module.Finite R M] (b : Basis ι R M) : Finite ι
 
Module.Finite.finite_basis: ∀ {R : Type u_6} {M : Type u_7} [inst : Semiring R] [inst_1 : Nontrivial R] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {ι : Type u_8} [inst_4 : Module.Finite R M], Basis ι R M → Finite ι
Module.Finite.finite_basis


Basis.ofVectorSpace.{u_3, u_4} (K : Type u_3) (V : Type u_4) [DivisionRing K] [AddCommGroup V] [Module K V] :
  Basis (↑(Basis.ofVectorSpaceIndex K V)) K V
 
Basis.ofVectorSpace: (K : Type u_3) →
  (V : Type u_4) →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] → [inst_2 : Module K V] → Basis (↑(Basis.ofVectorSpaceIndex K V)) K V
Basis.ofVectorSpace


Module.finBasis.{u, v} (R : Type u) (M : Type v) [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M]
  [Module.Free R M] [Module.Finite R M] : Basis (Fin (Module.finrank R M)) R M
 
Module.finBasis: (R : Type u) →
  (M : Type v) →
    [inst : Ring R] →
      [inst_1 : StrongRankCondition R] →
        [inst_2 : AddCommGroup M] →
          [inst_3 : Module R M] →
            [inst_4 : Module.Free R M] → [inst_5 : Module.Finite R M] → Basis (Fin (Module.finrank R M)) R M
Module.finBasis


Basis.ofVectorSpaceIndex.{u_3, u_4} (K : Type u_3) (V : Type u_4) [DivisionRing K] [AddCommGroup V] [Module K V] : Set V
 
Basis.ofVectorSpaceIndex: (K : Type u_3) → (V : Type u_4) → [inst : DivisionRing K] → [inst_1 : AddCommGroup V] → [inst : Module K V] → Set V
Basis.ofVectorSpaceIndex

/- The `Subgroup` generated by a set. -/
-- def closure (k : Set G) : Subgroup G :=
--   sInf { K | k ⊆ K }

Subgroup.closure.{u_1} {G : Type u_1} [Group G] (k : Set G) : Subgroup G
 
Subgroup.closure: {G : Type u_1} → [inst : Group G] → Set G → Subgroup G
Subgroup.closure

/- The span of a set `s ⊆ M` is the smallest submodule of M that contains `s`. -/
-- def span (s : Set M) : Submodule R M :=
--   sInf { p | s ⊆ p }

Submodule.span.{u_1, u_4} (R : Type u_1) {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) :
  Submodule R M
 
Submodule.span: (R : Type u_1) →
  {M : Type u_4} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Set M → Submodule R M
Submodule.span


Submodule R (ι →₀ R) : Type (max uR uι)
 
Submodule: (R : Type uR) →
  (M : Type (max uR uι)) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst : Module R M] → Type (max uR uι)
Submodule 
R: Type uR
R (
ι: Type uι
ι →₀ 
R: Type uR
R)


Finsupp.module ι R


/- Interprets (l : α →₀ R) as linear combination of the elements in the family (v : α → M) and
    evaluates this linear combination. -/
-- protected def total : (α →₀ R) →ₗ[R] M :=
--   Finsupp.lsum ℕ fun i => LinearMap.id.smulRight (v i)

Finsupp.total.{u_1, u_2, u_5} {α : Type u_1} {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M]
  (v : α → M) : (α →₀ R) →ₗ[R] M
 
Finsupp.total: {α : Type u_1} →
  {M : Type u_2} →
    (R : Type u_5) →
      [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (α → M) → (α →₀ R) →ₗ[R] M
Finsupp.total

/- `LinearIndependent R v` states the family of vectors `v` is linearly independent over `R`. -/
-- def LinearIndependent : Prop :=
--   LinearMap.ker (Finsupp.total ι M R v) = ⊥

LinearIndependent.{u', u_2, u_4} {ι : Type u'} (R : Type u_2) {M : Type u_4} (v : ι → M) [Semiring R] [AddCommMonoid M]
  [Module R M] : Prop
 
LinearIndependent: {ι : Type u'} →
  (R : Type u_2) →
    {M : Type u_4} → (ι → M) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst : Module R M] → Prop
LinearIndependent


Module.rank.{u_1, u_2} (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] : Cardinal.{u_2}
 
Module.rank: (R : Type u_1) →
  (M : Type u_2) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst : Module R M] → Cardinal.{u_2}
Module.rank


Module.Free.chooseBasis.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] :
  Basis (Module.Free.ChooseBasisIndex R M) R M
 
Module.Free.chooseBasis: (R : Type u) →
  (M : Type v) →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → [inst_3 : Module.Free R M] → Basis (Module.Free.ChooseBasisIndex R M) R M
Module.Free.chooseBasis


Basis.coord.{u_1, u_3, u_6} {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M]
  (b : Basis ι R M) (i : ι) : M →ₗ[R] R
 
Basis.coord: {ι : Type u_1} →
  {R : Type u_3} →
    {M : Type u_6} →
      [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Basis ι R M → ι → M →ₗ[R] R
Basis.coord


Basis.exists_basis.{u_3, u_4} (K : Type u_3) (V : Type u_4) [DivisionRing K] [AddCommGroup V] [Module K V] :
  ∃ s, Nonempty (Basis (↑s) K V)
 
Basis.exists_basis: ∀ (K : Type u_3) (V : Type u_4) [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
  ∃ s, Nonempty (Basis (↑s) K V)
Basis.exists_basis


DirectSum.{v, w} (ι : Type v) (β : ι → Type w) [(i : ι) → AddCommMonoid (β i)] : Type (max w v)
 
DirectSum: (ι : Type v) → (β : ι → Type w) → [inst : (i : ι) → AddCommMonoid (β i)] → Type (max w v)
DirectSum


Module.Free.directSum.{u, u_2, u_3} (R : Type u) [Semiring R] {ι : Type u_2} (M : ι → Type u_3)
  [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [∀ (i : ι), Module.Free R (M i)] :
  Module.Free R (DirectSum ι fun i => M i)
 
Module.Free.directSum: ∀ (R : Type u) [inst : Semiring R] {ι : Type u_2} (M : ι → Type u_3) [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : ∀ (i : ι), Module.Free R (M i)],
  Module.Free R (DirectSum ι fun i => M i)
Module.Free.directSum


DirectSum.instAlgebra.{uι, uR, uA} {ι : Type uι} (R : Type uR) (A : ι → Type uA) [CommSemiring R]
  [(i : ι) → AddCommMonoid (A i)] [(i : ι) → Module R (A i)] [AddMonoid ι] [DirectSum.GSemiring A]
  [DirectSum.GAlgebra R A] [DecidableEq ι] : Algebra R (DirectSum ι fun i => A i)
 
DirectSum.instAlgebra: {ι : Type uι} →
  (R : Type uR) →
    (A : ι → Type uA) →
      [inst : CommSemiring R] →
        [inst_1 : (i : ι) → AddCommMonoid (A i)] →
          [inst_2 : (i : ι) → Module R (A i)] →
            [inst_3 : AddMonoid ι] →
              [inst_4 : DirectSum.GSemiring A] →
                [inst_5 : DirectSum.GAlgebra R A] → [inst_6 : DecidableEq ι] → Algebra R (DirectSum ι fun i => A i)
DirectSum.instAlgebra


DirectSum.add_apply.{v, w} {ι : Type v} {β : ι → Type w} [(i : ι) → AddCommMonoid (β i)]
  (g₁ g₂ : DirectSum ι fun i => β i) (i : ι) : (g₁ + g₂) i = g₁ i + g₂ i
 
DirectSum.add_apply: ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] (g₁ g₂ : DirectSum ι fun i => β i) (i : ι),
  (g₁ + g₂) i = g₁ i + g₂ i
DirectSum.add_apply


LinearMap.{u_14, u_15, u_16, u_17} {R : Type u_14} {S : Type u_15} [Semiring R] [Semiring S] (σ : R →+* S)
  (M : Type u_16) (M₂ : Type u_17) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] :
  Type (max u_16 u_17)
 
LinearMap: {R : Type u_14} →
  {S : Type u_15} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        (R →+* S) →
          (M : Type u_16) →
            (M₂ : Type u_17) →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : AddCommMonoid M₂] → [inst : Module R M] → [inst : Module S M₂] → Type (max u_16 u_17)
LinearMap


LinearMap.ker.{u_1, u_2, u_5, u_7, u_11} {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [Semiring R]
  [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_11}
  [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] (f : F) : Submodule R M
 
LinearMap.ker: {R : Type u_1} →
  {R₂ : Type u_2} →
    {M : Type u_5} →
      {M₂ : Type u_7} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R₂ M₂] →
                    {τ₁₂ : R →+* R₂} →
                      {F : Type u_11} →
                        [inst_6 : FunLike F M M₂] → [inst_7 : SemilinearMapClass F τ₁₂ M M₂] → F → Submodule R M
LinearMap.ker


LinearMap.range.{u_1, u_2, u_5, u_6, u_10} {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Semiring R]
  [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_10}
  [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [RingHomSurjective τ₁₂] (f : F) : Submodule R₂ M₂
 
LinearMap.range: {R : Type u_1} →
  {R₂ : Type u_2} →
    {M : Type u_5} →
      {M₂ : Type u_6} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R₂ M₂] →
                    {τ₁₂ : R →+* R₂} →
                      {F : Type u_10} →
                        [inst_6 : FunLike F M M₂] →
                          [inst_7 : SemilinearMapClass F τ₁₂ M M₂] →
                            [inst : RingHomSurjective τ₁₂] → F → Submodule R₂ M₂
LinearMap.range


rank_range_add_rank_ker.{u, u_1} {R : Type u_1} {M M₁ : Type u} [Ring R] [AddCommGroup M] [AddCommGroup M₁] [Module R M]
  [Module R M₁] [HasRankNullity.{u, u_1} R] (f : M →ₗ[R] M₁) :
  Module.rank R ↥(LinearMap.range f) + Module.rank R ↥(LinearMap.ker f) = Module.rank R M
 
rank_range_add_rank_ker: ∀ {R : Type u_1} {M M₁ : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M₁]
  [inst_3 : Module R M] [inst_4 : Module R M₁] [inst_5 : HasRankNullity.{u, u_1} R] (f : M →ₗ[R] M₁),
  Module.rank R ↥(LinearMap.range f) + Module.rank R ↥(LinearMap.ker f) = Module.rank R M
rank_range_add_rank_ker


LinearEquiv.{u_12, u_13, u_14, u_15} {R : Type u_12} {S : Type u_13} [Semiring R] [Semiring S] (σ : R →+* S)
  {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (M : Type u_14) (M₂ : Type u_15) [AddCommMonoid M]
  [AddCommMonoid M₂] [Module R M] [Module S M₂] : Type (max u_14 u_15)
 
LinearEquiv: {R : Type u_12} →
  {S : Type u_13} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        (σ : R →+* S) →
          {σ' : S →+* R} →
            [inst_2 : RingHomInvPair σ σ'] →
              [inst_3 : RingHomInvPair σ' σ] →
                (M : Type u_14) →
                  (M₂ : Type u_15) →
                    [inst_4 : AddCommMonoid M] →
                      [inst_5 : AddCommMonoid M₂] → [inst : Module R M] → [inst : Module S M₂] → Type (max u_14 u_15)
LinearEquiv


Basis.map.{u_1, u_3, u_6, u_7} {ι : Type u_1} {R : Type u_3} {M : Type u_6} {M' : Type u_7} [Semiring R]
  [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (f : M ≃ₗ[R] M') : Basis ι R M'
 
Basis.map: {ι : Type u_1} →
  {R : Type u_3} →
    {M : Type u_6} →
      {M' : Type u_7} →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommMonoid M'] → [inst_4 : Module R M'] → Basis ι R M → (M ≃ₗ[R] M') → Basis ι R M'
Basis.map


LinearEquiv.ofRankEq.{u, v} {R : Type u} (M M₁ : Type v) [Ring R] [StrongRankCondition R] [AddCommGroup M] [Module R M]
  [Module.Free R M] [AddCommGroup M₁] [Module R M₁] [Module.Free R M₁] (cond : Module.rank R M = Module.rank R M₁) :
  M ≃ₗ[R] M₁
 
LinearEquiv.ofRankEq: {R : Type u} →
  (M M₁ : Type v) →
    [inst : Ring R] →
      [inst_1 : StrongRankCondition R] →
        [inst_2 : AddCommGroup M] →
          [inst_3 : Module R M] →
            [inst_4 : Module.Free R M] →
              [inst_5 : AddCommGroup M₁] →
                [inst_6 : Module R M₁] → [inst_7 : Module.Free R M₁] → Module.rank R M = Module.rank R M₁ → M ≃ₗ[R] M₁
LinearEquiv.ofRankEq


Module.End.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Type v
 
Module.End: (R : Type u) → (M : Type v) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst : Module R M] → Type v
Module.End


Module.End.semiring.{u_1, u_5} {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] :
  Semiring (Module.End R M)
 
Module.End.semiring: {R : Type u_1} →
  {M : Type u_5} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Semiring (Module.End R M)
Module.End.semiring

-- TODO: PR?
-- #check Module.End.algebra

Module.End.instAlgebra.{u, v, w} (R : Type u) (S : Type v) (M : Type w) [CommSemiring R] [Semiring S] [AddCommMonoid M]
  [Module R M] [Module S M] [SMulCommClass S R M] [SMul R S] [IsScalarTower R S M] : Algebra R (Module.End S M)
 
Module.End.instAlgebra: (R : Type u) →
  (S : Type v) →
    (M : Type w) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring S] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Module R M] →
              [inst_4 : Module S M] →
                [inst_5 : SMulCommClass S R M] →
                  [inst_6 : SMul R S] → [inst_7 : IsScalarTower R S M] → Algebra R (Module.End S M)
Module.End.instAlgebra


DistribMulAction.toLinearMap.{u_1, u_4, u_5} (R : Type u_1) {S : Type u_4} (M : Type u_5) [Semiring R] [AddCommMonoid M]
  [Module R M] [Monoid S] [DistribMulAction S M] [SMulCommClass S R M] (s : S) : M →ₗ[R] M
 
DistribMulAction.toLinearMap: (R : Type u_1) →
  {S : Type u_4} →
    (M : Type u_5) →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : Monoid S] → [inst_4 : DistribMulAction S M] → [inst_5 : SMulCommClass S R M] → S → M →ₗ[R] M
DistribMulAction.toLinearMap


DistribMulAction.toModuleEnd.{u_1, u_4, u_5} (R : Type u_1) {S : Type u_4} (M : Type u_5) [Semiring R] [AddCommMonoid M]
  [Module R M] [Monoid S] [DistribMulAction S M] [SMulCommClass S R M] : S →* Module.End R M
 
DistribMulAction.toModuleEnd: (R : Type u_1) →
  {S : Type u_4} →
    (M : Type u_5) →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : Monoid S] → [inst_4 : DistribMulAction S M] → [inst_5 : SMulCommClass S R M] → S →* Module.End R M
DistribMulAction.toModuleEnd


LinearMap.toMatrix.{u_1, u_3, u_4, u_5, u_6} {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n]
  [Finite m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁]
  [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) : (M₁ →ₗ[R] M₂) ≃ₗ[R] Matrix m n R
 
LinearMap.toMatrix: {R : Type u_1} →
  [inst : CommSemiring R] →
    {m : Type u_3} →
      {n : Type u_4} →
        [inst_1 : Fintype n] →
          [inst_2 : Finite m] →
            [inst_3 : DecidableEq n] →
              {M₁ : Type u_5} →
                {M₂ : Type u_6} →
                  [inst_4 : AddCommMonoid M₁] →
                    [inst_5 : AddCommMonoid M₂] →
                      [inst_6 : Module R M₁] →
                        [inst_7 : Module R M₂] → Basis n R M₁ → Basis m R M₂ → (M₁ →ₗ[R] M₂) ≃ₗ[R] Matrix m n R
LinearMap.toMatrix


linearMap_toMatrix_mul_basis_toMatrix.{u_1, u_2, u_4, u_5, u_6, u_9} {ι : Type u_1} {ι' : Type u_2} {κ' : Type u_4}
  {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type u_9} [AddCommMonoid N]
  [Module R N] (b : Basis ι R M) (b' : Basis ι' R M) (c' : Basis κ' R N) (f : M →ₗ[R] N) [Fintype ι'] [Fintype ι]
  [Finite κ'] [DecidableEq ι] [DecidableEq ι'] :
  (LinearMap.toMatrix b' c') f * b'.toMatrix ⇑b = (LinearMap.toMatrix b c') f
 
linearMap_toMatrix_mul_basis_toMatrix: ∀ {ι : Type u_1} {ι' : Type u_2} {κ' : Type u_4} {R : Type u_5} {M : Type u_6} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_9} [inst_3 : AddCommMonoid N] [inst_4 : Module R N]
  (b : Basis ι R M) (b' : Basis ι' R M) (c' : Basis κ' R N) (f : M →ₗ[R] N) [inst_5 : Fintype ι'] [inst_6 : Fintype ι]
  [inst_7 : Finite κ'] [inst_8 : DecidableEq ι] [inst_9 : DecidableEq ι'],
  (LinearMap.toMatrix b' c') f * b'.toMatrix ⇑b = (LinearMap.toMatrix b c') f
linearMap_toMatrix_mul_basis_toMatrix


Matrix.{u, u', v} (m : Type u) (n : Type u') (α : Type v) : Type (max u u' v)
 
Matrix: Type u → Type u' → Type v → Type (max u u' v)
Matrix

section

variable (
l: Type u
l 
m: Type u
m 
n: Type u
n: 
Type u: Type (u + 1)
Type u) (
α: Type uα
α : 
Type uα: Type (uα + 1)
Type uα) [
Fintype: Type u → Type u
Fintype 
l: Type u
l] [
Fintype: Type u → Type u
Fintype 
m: Type u
m] [
Fintype: Type u → Type u
Fintype 
n: Type u
n] [
Mul: Type uα → Type uα
Mul 
α: Type uα
α] [
AddCommMonoid: Type uα → Type uα
AddCommMonoid 
α: Type uα
α] (
x: Matrix l m α
x : 
Matrix: Type u → Type u → Type uα → Type (max u uα)
Matrix 
l: Type u
l 
m: Type u
m 
α: Type uα
α) (
y: Matrix m n α
y : 
Matrix: Type u → Type u → Type uα → Type (max u uα)
Matrix 
m: Type u
m 
n: Type u
n 
α: Type uα
α) (
z: Matrix l n α
z : 
Matrix: Type u → Type u → Type uα → Type (max u uα)
Matrix 
l: Type u
l 
n: Type u
n 
α: Type uα
α)


x * y : Matrix l n α
 
x: Matrix l m α
x * 
y: Matrix m n α
y


Matrix.instHMulOfFintypeOfMulOfAddCommMonoid


end


Matrix.instHMulOfFintypeOfMulOfAddCommMonoid.{v, u_1, u_2, u_3} {l : Type u_1} {m : Type u_2} {n : Type u_3}
  {α : Type v} [Fintype m] [Mul α] [AddCommMonoid α] : HMul (Matrix l m α) (Matrix m n α) (Matrix l n α)
 
Matrix.instHMulOfFintypeOfMulOfAddCommMonoid: {l : Type u_1} →
  {m : Type u_2} →
    {n : Type u_3} →
      {α : Type v} →
        [inst : Fintype m] →
          [inst : Mul α] → [inst : AddCommMonoid α] → HMul (Matrix l m α) (Matrix m n α) (Matrix l n α)
Matrix.instHMulOfFintypeOfMulOfAddCommMonoid


Matrix.mul_apply.{v, u_1, u_2, u_3} {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Mul α]
  [AddCommMonoid α] {M : Matrix l m α} {N : Matrix m n α} {i : l} {k : n} : (M * N) i k = ∑ j : m, M i j * N j k
 
Matrix.mul_apply: ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Fintype m] [inst_1 : Mul α]
  [inst_2 : AddCommMonoid α] {M : Matrix l m α} {N : Matrix m n α} {i : l} {k : n}, (M * N) i k = ∑ j : m, M i j * N j k
Matrix.mul_apply


Matrix.sum_apply.{v, w, u_2, u_3} {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [AddCommMonoid α] (i : m)
  (j : n) (s : Finset β) (g : β → Matrix m n α) : (∑ c ∈ s, g c) i j = ∑ c ∈ s, g c i j
 
Matrix.sum_apply: ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [inst : AddCommMonoid α] (i : m) (j : n) (s : Finset β)
  (g : β → Matrix m n α), (∑ c ∈ s, g c) i j = ∑ c ∈ s, g c i j
Matrix.sum_apply


Matrix.toLin.{u_1, u_3, u_4, u_5, u_6} {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n]
  [Finite m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁]
  [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) : Matrix m n R ≃ₗ[R] M₁ →ₗ[R] M₂
 
Matrix.toLin: {R : Type u_1} →
  [inst : CommSemiring R] →
    {m : Type u_3} →
      {n : Type u_4} →
        [inst_1 : Fintype n] →
          [inst_2 : Finite m] →
            [inst_3 : DecidableEq n] →
              {M₁ : Type u_5} →
                {M₂ : Type u_6} →
                  [inst_4 : AddCommMonoid M₁] →
                    [inst_5 : AddCommMonoid M₂] →
                      [inst_6 : Module R M₁] →
                        [inst_7 : Module R M₂] → Basis n R M₁ → Basis m R M₂ → Matrix m n R ≃ₗ[R] M₁ →ₗ[R] M₂
Matrix.toLin


Matrix.Represents.{u_1, u_2, u_3} {ι : Type u_1} [Fintype ι] {M : Type u_2} [AddCommGroup M] {R : Type u_3} [CommRing R]
  [Module R M] (b : ι → M) [DecidableEq ι] (A : Matrix ι ι R) (f : Module.End R M) : Prop
 
Matrix.Represents: {ι : Type u_1} →
  [inst : Fintype ι] →
    {M : Type u_2} →
      [inst : AddCommGroup M] →
        {R : Type u_3} →
          [inst_1 : CommRing R] →
            [inst_2 : Module R M] → (ι → M) → [inst_3 : DecidableEq ι] → Matrix ι ι R → Module.End R M → Prop
Matrix.Represents


Matrix.isRepresentation.{u_1, u_2, u_3} {ι : Type u_1} [Fintype ι] {M : Type u_2} [AddCommGroup M] (R : Type u_3)
  [CommRing R] [Module R M] (b : ι → M) [DecidableEq ι] : Subalgebra R (Matrix ι ι R)
 
Matrix.isRepresentation: {ι : Type u_1} →
  [inst : Fintype ι] →
    {M : Type u_2} →
      [inst_1 : AddCommGroup M] →
        (R : Type u_3) →
          [inst_2 : CommRing R] →
            [inst_3 : Module R M] → (ι → M) → [inst_4 : DecidableEq ι] → Subalgebra R (Matrix ι ι R)
Matrix.isRepresentation


Matrix.isRepresentation.toEnd.{u_1, u_2, u_3} {ι : Type u_1} [Fintype ι] {M : Type u_2} [AddCommGroup M] (R : Type u_3)
  [CommRing R] [Module R M] (b : ι → M) [DecidableEq ι] (hb : Submodule.span R (Set.range b) = ⊤) :
  ↥(Matrix.isRepresentation R b) →ₐ[R] Module.End R M
 
Matrix.isRepresentation.toEnd: {ι : Type u_1} →
  [inst : Fintype ι] →
    {M : Type u_2} →
      [inst_1 : AddCommGroup M] →
        (R : Type u_3) →
          [inst_2 : CommRing R] →
            [inst_3 : Module R M] →
              (b : ι → M) →
                [inst_4 : DecidableEq ι] →
                  Submodule.span R (Set.range b) = ⊤ → ↥(Matrix.isRepresentation R b) →ₐ[R] Module.End R M
Matrix.isRepresentation.toEnd


PiToModule.fromMatrix.{u_1, u_2, u_3} {ι : Type u_1} [Fintype ι] {M : Type u_2} [AddCommGroup M] (R : Type u_3)
  [CommRing R] [Module R M] (b : ι → M) [DecidableEq ι] : Matrix ι ι R →ₗ[R] (ι → R) →ₗ[R] M
 
PiToModule.fromMatrix: {ι : Type u_1} →
  [inst : Fintype ι] →
    {M : Type u_2} →
      [inst : AddCommGroup M] →
        (R : Type u_3) →
          [inst_1 : CommRing R] →
            [inst_2 : Module R M] → (ι → M) → [inst_3 : DecidableEq ι] → Matrix ι ι R →ₗ[R] (ι → R) →ₗ[R] M
PiToModule.fromMatrix


Matrix.inv.{u', v} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] : Inv (Matrix n n α)
 
Matrix.inv: {n : Type u'} → {α : Type v} → [inst : Fintype n] → [inst : DecidableEq n] → [inst : CommRing α] → Inv (Matrix n n α)
Matrix.inv


Matrix.invOf_eq.{u', v} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α)
  [Invertible A.det] [Invertible A] : ⅟A = ⅟A.det • A.adjugate
 
Matrix.invOf_eq: ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α)
  [inst_3 : Invertible A.det] [inst_4 : Invertible A], ⅟A = ⅟A.det • A.adjugate
Matrix.invOf_eq


Matrix.invOf_eq_nonsing_inv.{u', v} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α]
  (A : Matrix n n α) [Invertible A] : ⅟A = A⁻¹
 
Matrix.invOf_eq_nonsing_inv: ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α)
  [inst_3 : Invertible A], ⅟A = A⁻¹
Matrix.invOf_eq_nonsing_inv


Matrix.invertibleOfDetInvertible.{u', v} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α]
  (A : Matrix n n α) [Invertible A.det] : Invertible A
 
Matrix.invertibleOfDetInvertible: {n : Type u'} →
  {α : Type v} →
    [inst : Fintype n] →
      [inst_1 : DecidableEq n] → [inst_2 : CommRing α] → (A : Matrix n n α) → [inst_3 : Invertible A.det] → Invertible A
Matrix.invertibleOfDetInvertible

-- TODO: an endomorphism is invertible iff the matrix is invertible


algEquivMatrix.{u_1, u_2, u_3} {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] {M : Type u_3}
  [AddCommGroup M] [Module R M] [Fintype n] (h : Basis n R M) : Module.End R M ≃ₐ[R] Matrix n n R
 
algEquivMatrix: {R : Type u_1} →
  [inst : CommRing R] →
    {n : Type u_2} →
      [inst_1 : DecidableEq n] →
        {M : Type u_3} →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Module R M] → [inst_4 : Fintype n] → Basis n R M → Module.End R M ≃ₐ[R] Matrix n n R
algEquivMatrix

-- change of basis matrix

basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix.{u_1, u_2, u_3, u_4, u_5, u_6, u_9} {ι : Type u_1}
  {ι' : Type u_2} {κ : Type u_3} {κ' : Type u_4} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M]
  [Module R M] {N : Type u_9} [AddCommMonoid N] [Module R N] (b : Basis ι R M) (b' : Basis ι' R M) (c : Basis κ R N)
  (c' : Basis κ' R N) (f : M →ₗ[R] N) [Fintype ι'] [Finite κ] [Fintype ι] [Fintype κ'] [DecidableEq ι]
  [DecidableEq ι'] : c.toMatrix ⇑c' * (LinearMap.toMatrix b' c') f * b'.toMatrix ⇑b = (LinearMap.toMatrix b c) f
 
basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix: ∀ {ι : Type u_1} {ι' : Type u_2} {κ : Type u_3} {κ' : Type u_4} {R : Type u_5} {M : Type u_6} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_9} [inst_3 : AddCommMonoid N] [inst_4 : Module R N]
  (b : Basis ι R M) (b' : Basis ι' R M) (c : Basis κ R N) (c' : Basis κ' R N) (f : M →ₗ[R] N) [inst_5 : Fintype ι']
  [inst_6 : Finite κ] [inst_7 : Fintype ι] [inst_8 : Fintype κ'] [inst_9 : DecidableEq ι] [inst_10 : DecidableEq ι'],
  c.toMatrix ⇑c' * (LinearMap.toMatrix b' c') f * b'.toMatrix ⇑b = (LinearMap.toMatrix b c) f
basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix


Module.End.eigenspace.{v, w} {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M)
  (μ : R) : Submodule R M
 
Module.End.eigenspace: {R : Type v} →
  {M : Type w} →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Module.End R M → R → Submodule R M
Module.End.eigenspace


Module.End.HasEigenvalue.{v, w} {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M]
  (f : Module.End R M) (a : R) : Prop
 
Module.End.HasEigenvalue: {R : Type v} →
  {M : Type w} → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Module.End R M → R → Prop
Module.End.HasEigenvalue


Module.End.HasEigenvector.{v, w} {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M]
  (f : Module.End R M) (μ : R) (x : M) : Prop
 
Module.End.HasEigenvector: {R : Type v} →
  {M : Type w} → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Module.End R M → R → M → Prop
Module.End.HasEigenvector


Module.End.Eigenvalues.{v, w} {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M]
  (f : Module.End R M) : Type v
 
Module.End.Eigenvalues: {R : Type v} →
  {M : Type w} → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Module.End R M → Type v
Module.End.Eigenvalues

/- The generalized eigenspace for a linear map `f`, a scalar `μ`, and an exponent `k ∈ ℕ` is the
kernel of `(f - μ • id) ^ k`. (Def 8.10 of [axler2015]). Furthermore, a generalized eigenspace for
some exponent `k` is contained in the generalized eigenspace for exponents larger than `k`. -/
-- def generalizedEigenspace (f : End R M) (μ : R) : ℕ →o Submodule R M where
--   toFun k := LinearMap.ker ((f - algebraMap R (End R M) μ) ^ k)
--   monotone' k m hm := by
--     simp only [← pow_sub_mul_pow _ hm]
--     exact
--       LinearMap.ker_le_ker_comp ((f - algebraMap R (End R M) μ) ^ k)
--         ((f - algebraMap R (End R M) μ) ^ (m - k))

Module.End.genEigenspace.{v, w} {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M]
  (f : Module.End R M) (μ : R) : ℕ →o Submodule R M
 
Module.End.genEigenspace: {R : Type v} →
  {M : Type w} →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Module.End R M → R → ℕ →o Submodule R M
Module.End.genEigenspace


OrderHom.{u_6, u_7} (α : Type u_6) (β : Type u_7) [Preorder α] [Preorder β] : Type (max u_6 u_7)
 
OrderHom: (α : Type u_6) → (β : Type u_7) → [inst : Preorder α] → [inst : Preorder β] → Type (max u_6 u_7)
OrderHom


Module.End.eigenspaces_independent.{v, w} {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M]
  [NoZeroSMulDivisors R M] (f : Module.End R M) : CompleteLattice.Independent f.eigenspace
 
Module.End.eigenspaces_independent: ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : NoZeroSMulDivisors R M] (f : Module.End R M), CompleteLattice.Independent f.eigenspace
Module.End.eigenspaces_independent


Module.End.eigenvectors_linearIndependent.{v, w} {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M]
  [NoZeroSMulDivisors R M] (f : Module.End R M) (μs : Set R) (xs : ↑μs → M)
  (h_eigenvec : ∀ (μ : ↑μs), f.HasEigenvector (↑μ) (xs μ)) : LinearIndependent (ι := ↑μs) R xs
 
Module.End.eigenvectors_linearIndependent: ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : NoZeroSMulDivisors R M] (f : Module.End R M) (μs : Set R) (xs : ↑μs → M),
  (∀ (μ : ↑μs), f.HasEigenvector (↑μ) (xs μ)) → LinearIndependent (ι := ↑μs) R xs
Module.End.eigenvectors_linearIndependent


Module.End.exists_eigenvalue.{u_1, u_2} {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V]
  [IsAlgClosed K] [FiniteDimensional K V] [Nontrivial V] (f : Module.End K V) : ∃ c, f.HasEigenvalue c
 
Module.End.exists_eigenvalue: ∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : IsAlgClosed K] [inst_4 : FiniteDimensional K V] [inst_5 : Nontrivial V] (f : Module.End K V),
  ∃ c, f.HasEigenvalue c
Module.End.exists_eigenvalue


Matrix.IsHermitian.det_eq_prod_eigenvalues.{u_1, u_2} {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n]
  {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) : A.det = ∏ i : n, ↑(hA.eigenvalues i)
 
Matrix.IsHermitian.det_eq_prod_eigenvalues: ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n]
  (hA : A.IsHermitian), A.det = ∏ i : n, ↑(hA.eigenvalues i)
Matrix.IsHermitian.det_eq_prod_eigenvalues


Basis.det.{u_1, u_2, u_4} {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_4}
  [DecidableEq ι] [Fintype ι] (e : Basis ι R M) : M [⋀^ι]→ₗ[R] R
 
Basis.det: {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {ι : Type u_4} → [inst_3 : DecidableEq ι] → [inst_4 : Fintype ι] → Basis ι R M → M [⋀^ι]→ₗ[R] R
Basis.det


LinearMap.det.{u_7, u_8} {M : Type u_7} [AddCommGroup M] {A : Type u_8} [CommRing A] [Module A M] : (M →ₗ[A] M) →* A
 
LinearMap.det: {M : Type u_7} →
  [inst : AddCommGroup M] → {A : Type u_8} → [inst_1 : CommRing A] → [inst_2 : Module A M] → (M →ₗ[A] M) →* A
LinearMap.det


Subgroup.zpowers.{u_1} {G : Type u_1} [Group G] (g : G) : Subgroup G
 
Subgroup.zpowers: {G : Type u_1} → [inst : Group G] → G → Subgroup G
Subgroup.zpowers


IsFreeGroup.Generators.{u_1} (G : Type u_1) [Group G] [IsFreeGroup G] : Type u_1
 
IsFreeGroup.Generators: (G : Type u_1) → [inst : Group G] → [inst : IsFreeGroup G] → Type u_1
IsFreeGroup.Generators


Matrix.diag.{v, u_3} {n : Type u_3} {α : Type v} (A : Matrix n n α) (i : n) : α
 
Matrix.diag: {n : Type u_3} → {α : Type v} → Matrix n n α → n → α
Matrix.diag


Matrix.diagonal.{v, u_3} {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] (d : n → α) : Matrix n n α
 
Matrix.diagonal: {n : Type u_3} → {α : Type v} → [inst : DecidableEq n] → [inst : Zero α] → (n → α) → Matrix n n α
Matrix.diagonal


LinearMap.IsProj.{u_5, u_6, u_7} {S : Type u_5} [Semiring S] {M : Type u_6} [AddCommMonoid M] [Module S M]
  (m : Submodule S M) {F : Type u_7} [FunLike F M M] (f : F) : Prop
 
LinearMap.IsProj: {S : Type u_5} →
  [inst : Semiring S] →
    {M : Type u_6} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module S M] → Submodule S M → {F : Type u_7} → [inst : FunLike F M M] → F → Prop
LinearMap.IsProj


LinearMap.isProj_iff_idempotent.{u_5, u_6} {S : Type u_5} [Semiring S] {M : Type u_6} [AddCommMonoid M] [Module S M]
  (f : M →ₗ[S] M) : (∃ p, LinearMap.IsProj p f) ↔ f ∘ₗ f = f
 
LinearMap.isProj_iff_idempotent: ∀ {S : Type u_5} [inst : Semiring S] {M : Type u_6} [inst_1 : AddCommMonoid M] [inst_2 : Module S M] (f : M →ₗ[S] M),
  (∃ p, LinearMap.IsProj p f) ↔ f ∘ₗ f = f
LinearMap.isProj_iff_idempotent

-- TODO: л is projection of a vector space V. Then V = Im л 0 Ker л.


Submodule.prod.{u_1, u_4, u_9} {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M]
  (p : Submodule R M) {M' : Type u_9} [AddCommMonoid M'] [Module R M'] (q₁ : Submodule R M') : Submodule R (M × M')
 
Submodule.prod: {R : Type u_1} →
  {M : Type u_4} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          Submodule R M →
            {M' : Type u_9} →
              [inst_3 : AddCommMonoid M'] → [inst_4 : Module R M'] → Submodule R M' → Submodule R (M × M')
Submodule.prod


LinearMap.coprod.{u, v, w, y} {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [Semiring R] [AddCommMonoid M]
  [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) :
  M × M₂ →ₗ[R] M₃
 
LinearMap.coprod: {R : Type u} →
  {M : Type v} →
    {M₂ : Type w} →
      {M₃ : Type y} →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : AddCommMonoid M₃] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R M₂] → [inst_6 : Module R M₃] → (M →ₗ[R] M₃) → (M₂ →ₗ[R] M₃) → M × M₂ →ₗ[R] M₃
LinearMap.coprod


Matrix.GeneralLinearGroup.{u, v} (n : Type u) (R : Type v) [DecidableEq n] [Fintype n] [CommRing R] : Type (max v u)
 
Matrix.GeneralLinearGroup: (n : Type u) → (R : Type v) → [inst : DecidableEq n] → [inst : Fintype n] → [inst : CommRing R] → Type (max v u)
Matrix.GeneralLinearGroup


Matrix.ext.{v, u_2, u_3} {m : Type u_2} {n : Type u_3} {α : Type v} {M N : Matrix m n α} :
  (∀ (i : m) (j : n), M i j = N i j) → M = N
 
Matrix.ext: ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {M N : Matrix m n α}, (∀ (i : m) (j : n), M i j = N i j) → M = N
Matrix.ext


Representation.{u_1, u_2, u_3} (k : Type u_1) (G : Type u_2) (V : Type u_3) [CommSemiring k] [Monoid G]
  [AddCommMonoid V] [Module k V] : Type (max u_2 u_3)
 
Representation: (k : Type u_1) →
  (G : Type u_2) →
    (V : Type u_3) →
      [inst : CommSemiring k] →
        [inst_1 : Monoid G] → [inst_2 : AddCommMonoid V] → [inst : Module k V] → Type (max u_2 u_3)
Representation


Representation.asGroupHom.{u_1, u_2, u_3} {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G]
  [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : G →* (V →ₗ[k] V)ˣ
 
Representation.asGroupHom: {k : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : CommSemiring k] →
        [inst_1 : Group G] →
          [inst_2 : AddCommMonoid V] → [inst_3 : Module k V] → Representation k G V → G →* (V →ₗ[k] V)ˣ
Representation.asGroupHom


Representation.asAlgebraHom.{u_1, u_2, u_3} {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G]
  [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : MonoidAlgebra k G →ₐ[k] Module.End k V
 
Representation.asAlgebraHom: {k : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : CommSemiring k] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid V] →
            [inst_3 : Module k V] → Representation k G V → MonoidAlgebra k G →ₐ[k] Module.End k V
Representation.asAlgebraHom


Representation.asModuleEquiv.{u_1, u_2, u_3} {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G]
  [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : ρ.asModule ≃+ V
 
Representation.asModuleEquiv: {k : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : CommSemiring k] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid V] → [inst_3 : Module k V] → (ρ : Representation k G V) → ρ.asModule ≃+ V
Representation.asModuleEquiv


Representation.ofMulAction.{u_1, u_2, u_3} (k : Type u_1) [CommSemiring k] (G : Type u_2) [Monoid G] (H : Type u_3)
  [MulAction G H] : Representation k G (H →₀ k)
 
Representation.ofMulAction: (k : Type u_1) →
  [inst : CommSemiring k] →
    (G : Type u_2) → [inst_1 : Monoid G] → (H : Type u_3) → [inst_2 : MulAction G H] → Representation k G (H →₀ k)
Representation.ofMulAction


Representation.ofDistribMulAction.{u_1, u_2, u_3} (k : Type u_1) (G : Type u_2) (A : Type u_3) [CommSemiring k]
  [Monoid G] [AddCommMonoid A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] : Representation k G A
 
Representation.ofDistribMulAction: (k : Type u_1) →
  (G : Type u_2) →
    (A : Type u_3) →
      [inst : CommSemiring k] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid A] →
            [inst_3 : Module k A] →
              [inst_4 : DistribMulAction G A] → [inst_5 : SMulCommClass G k A] → Representation k G A
Representation.ofDistribMulAction


Representation.linHom.{u_1, u_2, u_3, u_4} {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring k]
  [Group G] [AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] (ρV : Representation k G V)
  (ρW : Representation k G W) : Representation k G (V →ₗ[k] W)
 
Representation.linHom: {k : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : CommSemiring k] →
          [inst_1 : Group G] →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : Module k V] →
                [inst_4 : AddCommMonoid W] →
                  [inst_5 : Module k W] → Representation k G V → Representation k G W → Representation k G (V →ₗ[k] W)
Representation.linHom


[Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv]
 
QuadraticMap.isometryEquivBasisRepr: {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_4} →
      {N : Type u_9} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid N] →
              [inst_3 : Module R M] →
                [inst_4 : Module R N] →
                  [inst_5 : Finite ι] → (Q : QuadraticMap R M N) → (v : Basis ι R M) → Q.IsometryEquiv (Q.basisRepr v)
QuadraticMap.isometryEquivBasisRepr

-- section

-- variable {k G V: Type*}  [CommRing k] [Monoid G] [AddCommMonoid V] [Module k V]

-- variable (n : Type uN) [DecidableEq n] [Fintype n]

-- variable (ρ₁ ρ₂ : Representation k G V) (T' : Matrix.GeneralLinearGroup n k)

-- #check T'⁻¹

-- #check Matrix.GeneralLinearGroup.toLin T'

-- def Representation.equivalent : Prop :=
--   ∃ T : Matrix.GeneralLinearGroup n k,
--     ∀ g, ρ₁ g = T⁻¹ ∘ₗ ρ₂ g ∘ₗ T
-- end


Representation.trivial.{u_1, u_2, u_3} (k : Type u_1) {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G]
  [AddCommMonoid V] [Module k V] : Representation k G V
 
Representation.trivial: (k : Type u_1) →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : CommSemiring k] →
        [inst_1 : Monoid G] → [inst_2 : AddCommMonoid V] → [inst_3 : Module k V] → Representation k G V
Representation.trivial


CategoryTheory.Faithful.of_iso.{v₁, v₂, u₁, u₂} {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
  [CategoryTheory.Category.{v₂, u₂} D] {F F' : CategoryTheory.Functor C D} [F.Faithful] (α : F ≅ F') : F'.Faithful
 
CategoryTheory.Faithful.of_iso: ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F F' : CategoryTheory.Functor C D} [inst_2 : F.Faithful], (F ≅ F') → F'.Faithful
CategoryTheory.Faithful.of_iso


-- #check Real.cos -1

-- #check Real.cos (-1 : ℝ)

-- #check Complex.cos (-1 : ℂ)

-- example : Real.sqrt 1 = 1 := by
--   norm_num

-- example : Real.sqrt 1 = 1 ^ (1 / 2 : ℝ) := by
--   norm_num
--   done

-- example : (Real.sqrt 2)^2 = (2 : ℝ) := by
--   norm_num
--   done -- works

-- example : Real.sqrt 2 = 2 ^ (1 / 2) → false := by
--   norm_num
--   done -- works

-- example : Real.sqrt 2 = 2 ^ (1 / 2 : ℝ) := by
--   norm_num
--   done -- fails

-- example : Real.sqrt 2 = 2 ^ (1 / 2 : ℚ) := by
--   norm_num

--   done

-- example : Real.sqrt (-1 : ℝ ) = Real.sqrt (-4 : ℝ ) := by
--   norm_num
--   done

-- example : (2 : ℝ) * Real.sqrt (-1 : ℝ ) = Real.sqrt (-4 : ℝ ) := by
--   norm_num
--   done

-- TODO: FG-module

-- TODO: permutation module



MonoidAlgebra.{u₁, u₂} (k : Type u₁) (G : Type u₂) [Semiring k] : Type (max u₁ u₂)
 
MonoidAlgebra: (k : Type u₁) → Type u₂ → [inst : Semiring k] → Type (max u₁ u₂)
MonoidAlgebra


LinearMap.trace.{u, v} (R : Type u) [CommSemiring R] (M : Type v) [AddCommMonoid M] [Module R M] : (M →ₗ[R] M) →ₗ[R] R
 
LinearMap.trace: (R : Type u) →
  [inst : CommSemiring R] → (M : Type v) → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (M →ₗ[R] M) →ₗ[R] R
LinearMap.trace


LinearMap.trace_eq_matrix_trace.{u, v, w} (R : Type u) [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M]
  {ι : Type w} [DecidableEq ι] [Fintype ι] (b : Basis ι R M) (f : M →ₗ[R] M) :
  (LinearMap.trace R M) f = ((LinearMap.toMatrix b b) f).trace
 
LinearMap.trace_eq_matrix_trace: ∀ (R : Type u) [inst : CommSemiring R] {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type w}
  [inst_3 : DecidableEq ι] [inst_4 : Fintype ι] (b : Basis ι R M) (f : M →ₗ[R] M),
  (LinearMap.trace R M) f = ((LinearMap.toMatrix b b) f).trace
LinearMap.trace_eq_matrix_trace


LinearMap.trace_eq_contract.{u_1, u_2} (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M]
  [Module.Free R M] [Module.Finite R M] : LinearMap.trace R M ∘ₗ dualTensorHom R M M = contractLeft R M
 
LinearMap.trace_eq_contract: ∀ (R : Type u_1) [inst : CommRing R] (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : Module.Free R M] [inst_4 : Module.Finite R M], LinearMap.trace R M ∘ₗ dualTensorHom R M M = contractLeft R M
LinearMap.trace_eq_contract


LinearMap.baseChange.{u_1, u_2, u_4, u_5} {R : Type u_1} (A : Type u_2) {M : Type u_4} {N : Type u_5} [CommSemiring R]
  [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M →ₗ[R] N) :
  TensorProduct R A M →ₗ[A] TensorProduct R A N
 
LinearMap.baseChange: {R : Type u_1} →
  (A : Type u_2) →
    {M : Type u_4} →
      {N : Type u_5} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : AddCommMonoid M] →
                [inst_4 : AddCommMonoid N] →
                  [inst_5 : Module R M] →
                    [inst_6 : Module R N] → (M →ₗ[R] N) → TensorProduct R A M →ₗ[A] TensorProduct R A N
LinearMap.baseChange


LinearMap.trace_eq_contract_of_basis.{u_1, u_2, u_5} {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M]
  [Module R M] {ι : Type u_5} [Finite ι] (b : Basis ι R M) :
  LinearMap.trace R M ∘ₗ dualTensorHom R M M = contractLeft R M
 
LinearMap.trace_eq_contract_of_basis: ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_5}
  [inst_3 : Finite ι], Basis ι R M → LinearMap.trace R M ∘ₗ dualTensorHom R M M = contractLeft R M
LinearMap.trace_eq_contract_of_basis


alternatingGroup (Fin 8) : Subgroup (Equiv.Perm (Fin 8))
 
alternatingGroup: (α : Type) → [inst : Fintype α] → [inst : DecidableEq α] → Subgroup (Equiv.Perm α)
alternatingGroup (
Fin: ℕ → Type
Fin 
8: ℕ
8)

variable (
n: ℕ
n : 
ℕ: Type
ℕ)
abbrev 
Aₙ: Matrix (Fin n) (Fin n) ℕ
Aₙ : 
Matrix: Type → Type → Type → Type
Matrix (
Fin: ℕ → Type
Fin 
n: ℕ
n) (
Fin: ℕ → Type
Fin 
n: ℕ
n) 
ℕ: Type
ℕ := 
Matrix.of: {m n α : Type} → (m → n → α) ≃ Matrix m n α
Matrix.of fun 
i: Fin n
i 
j: Fin n
j : 
Fin: ℕ → Type
Fin 
n: ℕ
n =>
    if 
i: Fin n
i == 
j: Fin n
j then 
1: ℕ
1
      else (if 
i: Fin n
i == 
n: ℕ
n - 
1: ℕ
1 ∨ 
j: Fin n
j == 
n: ℕ
n - 
1: ℕ
1 then 
2: ℕ
2 else 
3: ℕ
3)


Aₙ 8 : Matrix (Fin 8) (Fin 8) ℕ
 
Aₙ: (n : ℕ) → Matrix (Fin n) (Fin n) ℕ
Aₙ 
8: ℕ
8


QuaternionGroup 8 : Type
 
QuaternionGroup: ℕ → Type
QuaternionGroup 
8: ℕ
8

-- https://en.wikipedia.org/wiki/Quaternion_group
-- https://kconrad.math.uconn.edu/blurbs/grouptheory/genquat.pdf
-- https://math.stackexchange.com/questions/305455/generalized-quaternion-group
abbrev 
Q₈: Type
Q₈ := 
QuaternionGroup: ℕ → Type
QuaternionGroup 
2: ℕ
2

abbrev 
C₃: Type
C₃ := 
Multiplicative: Type → Type
Multiplicative (
ZMod: ℕ → Type
ZMod 
3: ℕ
3)

-- variable (z : Z₃)

-- #synth Group Z₃

-- variable {C₃ : Type} [Group C₃] [Fintype C₃] (h : Fintype.card C₃ = 3) [IsCyclic C₃]

-- #check C₃


ZMod.commRing 3



AddGroupWithOne.toAddGroup



Multiplicative.group.{u} {α : Type u} [AddGroup α] : Group (Multiplicative α)
 
Multiplicative.group: {α : Type u} → [inst : AddGroup α] → Group (Multiplicative α)
Multiplicative.group


Multiplicative.commGroup



isCyclic_multiplicative



3

 
Fintype.card: (α : Type) → [inst : Fintype α] → ℕ
Fintype.card 
C₃: Type
C₃

-- #eval orderOf C₃


Additive.ofMul (Multiplicative (ZMod 3)) : Additive Type
 
Additive.ofMul: {α : Type 1} → α ≃ Additive α
Additive.ofMul <| 
Multiplicative: Type → Type
Multiplicative (
ZMod: ℕ → Type
ZMod 
3: ℕ
3)


Multiplicative.toAdd (Multiplicative (ZMod 3)) : Type
 
Multiplicative.toAdd: {α : Type 1} → Multiplicative α ≃ α
Multiplicative.toAdd <| 
Multiplicative: Type → Type
Multiplicative <| 
ZMod: ℕ → Type
ZMod 
3: ℕ
3

-- #synth AddGroup <| Multiplicative.toAdd <| Multiplicative <| ZMod 3


isCyclic_multiplicative



QuaternionGroup.instGroup



MulAut.conj.{u_3} {G : Type u_3} [Group G] : G →* MulAut G
 
MulAut.conj: {G : Type u_3} → [inst : Group G] → G →* MulAut G
MulAut.conj


RingEquiv.{u_7, u_8} (R : Type u_7) (S : Type u_8) [Mul R] [Mul S] [Add R] [Add S] : Type (max u_7 u_8)
 
RingEquiv: (R : Type u_7) → (S : Type u_8) → [inst : Mul R] → [inst : Mul S] → [inst : Add R] → [inst : Add S] → Type (max u_7 u_8)
RingEquiv


SMul.{u, v} (M : Type u) (α : Type v) : Type (max u v)
 
SMul: Type u → Type v → Type (max u v)
SMul


MulAction.{u_9, u_10} (α : Type u_9) (β : Type u_10) [Monoid α] : Type (max u_10 u_9)
 
MulAction: (α : Type u_9) → Type u_10 → [inst : Monoid α] → Type (max u_10 u_9)
MulAction


DistribMulAction.{u_7, u_8} (M : Type u_7) (A : Type u_8) [Monoid M] [AddMonoid A] : Type (max u_7 u_8)
 
DistribMulAction: (M : Type u_7) → (A : Type u_8) → [inst : Monoid M] → [inst : AddMonoid A] → Type (max u_7 u_8)
DistribMulAction


LinearPMap.{u, v, w} (R : Type u) [Ring R] (E : Type v) [AddCommGroup E] [Module R E] (F : Type w) [AddCommGroup F]
  [Module R F] : Type (max v w)
 
LinearPMap: (R : Type u) →
  [inst : Ring R] →
    (E : Type v) →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Module R E] → (F : Type w) → [inst_3 : AddCommGroup F] → [inst : Module R F] → Type (max v w)
LinearPMap


LinearPMap.instMulAction.{u_1, u_2, u_3, u_5} {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E]
  {F : Type u_3} [AddCommGroup F] [Module R F] {M : Type u_5} [Monoid M] [DistribMulAction M F] [SMulCommClass R M F] :
  MulAction M (E →ₗ.[R] F)
 
LinearPMap.instMulAction: {R : Type u_1} →
  [inst : Ring R] →
    {E : Type u_2} →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Module R E] →
          {F : Type u_3} →
            [inst_3 : AddCommGroup F] →
              [inst_4 : Module R F] →
                {M : Type u_5} →
                  [inst_5 : Monoid M] →
                    [inst_6 : DistribMulAction M F] → [inst_7 : SMulCommClass R M F] → MulAction M (E →ₗ.[R] F)
LinearPMap.instMulAction

-- #check ​Equiv.Perm

-- instance : MulAction C₃ Q₈ where
--   smul g h :=

def 
c1: C₃
c1 : 
C₃: Type
C₃ := 
1: C₃
1


0

 
c1: C₃
c1.
val: {n : ℕ} → ZMod n → ℕ
val

def 
f: ℕ → ZMod 3
f (
n: ℕ
n : 
ℕ: Type
ℕ) : 
ZMod: ℕ → Type
ZMod 
3: ℕ
3 := 
n: ℕ
n % 
3: ZMod 3
3


0

 
f: ℕ → ZMod 3
f 
0: ℕ
0


1

 
f: ℕ → ZMod 3
f 
1: ℕ
1


2

 
f: ℕ → ZMod 3
f 
2: ℕ
2

/-
0
-/

0

 
f: ℕ → ZMod 3
f 
3: ℕ
3


2

 
f: ℕ → ZMod 3
f 
2: ℕ
2 |>.
val: {n : ℕ} → ZMod n → ℕ
val

/-
8
-/

8

 
Fintype.card: (α : Type) → [inst : Fintype α] → ℕ
Fintype.card 
Q₈: Type
Q₈

-- TODO: typo Multiplication of the dihedral group PR

def 
e: Q₈
e : 
Q₈: Type
Q₈ := 
QuaternionGroup.a: {n : ℕ} → ZMod (2 * n) → QuaternionGroup n
QuaternionGroup.a 
0: ZMod (2 * 2)
0

def 
i: Q₈
i : 
Q₈: Type
Q₈ := 
QuaternionGroup.a: {n : ℕ} → ZMod (2 * n) → QuaternionGroup n
QuaternionGroup.a 
1: ZMod (2 * 2)
1

def 
ne: Q₈
ne : 
Q₈: Type
Q₈ := 
QuaternionGroup.a: {n : ℕ} → ZMod (2 * n) → QuaternionGroup n
QuaternionGroup.a 
2: ZMod (2 * 2)
2

def 
ni: Q₈
ni : 
Q₈: Type
Q₈ := 
QuaternionGroup.a: {n : ℕ} → ZMod (2 * n) → QuaternionGroup n
QuaternionGroup.a 
3: ZMod (2 * 2)
3

def 
j: Q₈
j : 
Q₈: Type
Q₈ := 
QuaternionGroup.xa: {n : ℕ} → ZMod (2 * n) → QuaternionGroup n
QuaternionGroup.xa 
0: ZMod (2 * 2)
0

def 
nk: Q₈
nk : 
Q₈: Type
Q₈ := 
QuaternionGroup.xa: {n : ℕ} → ZMod (2 * n) → QuaternionGroup n
QuaternionGroup.xa 
1: ZMod (2 * 2)
1

def 
nj: Q₈
nj : 
Q₈: Type
Q₈ := 
QuaternionGroup.xa: {n : ℕ} → ZMod (2 * n) → QuaternionGroup n
QuaternionGroup.xa 
2: ZMod (2 * 2)
2

def 
k: Q₈
k : 
Q₈: Type
Q₈ := 
QuaternionGroup.xa: {n : ℕ} → ZMod (2 * n) → QuaternionGroup n
QuaternionGroup.xa 
3: ZMod (2 * 2)
3

def 
QuaternionGroup.f: Q₈ → Q₈
QuaternionGroup.f : 
Q₈: Type
Q₈ → 
Q₈: Type
Q₈
  | 
a: {n : ℕ} → ZMod (2 * n) → QuaternionGroup n
a 
1: ZMod (2 * 2)
1 => 
xa: {n : ℕ} → ZMod (2 * n) → QuaternionGroup n
xa 
0: ZMod (2 * 2)
0   -- i -> j
  | 
xa: {n : ℕ} → ZMod (2 * n) → QuaternionGroup n
xa 
0: ZMod (2 * 2)
0 => 
xa: {n : ℕ} → ZMod (2 * n) → QuaternionGroup n
xa 
3: ZMod (2 * 2)
3  -- j -> k
  | 
xa: {n : ℕ} → ZMod (2 * n) → QuaternionGroup n
xa 
3: ZMod (2 * 2)
3 => 
a: {n : ℕ} → ZMod (2 * n) → QuaternionGroup n
a 
1: ZMod (2 * 2)
1   -- k -> i
  | 
a: {n : ℕ} → ZMod (2 * n) → QuaternionGroup n
a 
3: ZMod (2 * 2)
3 => 
xa: {n : ℕ} → ZMod (2 * n) → QuaternionGroup n
xa 
2: ZMod (2 * 2)
2   -- ni -> nj
  | 
xa: {n : ℕ} → ZMod (2 * n) → QuaternionGroup n
xa 
2: ZMod (2 * 2)
2 => 
xa: {n : ℕ} → ZMod (2 * n) → QuaternionGroup n
xa 
1: ZMod (2 * 2)
1  -- nj -> nk
  | 
xa: {n : ℕ} → ZMod (2 * n) → QuaternionGroup n
xa 
1: ZMod (2 * 2)
1 => 
a: {n : ℕ} → ZMod (2 * n) → QuaternionGroup n
a 
3: ZMod (2 * 2)
3   -- nk -> ni
  | 
x: Q₈
x => 
x: Q₈
x        -- e, ne


ZMod.card (n : ℕ) [Fintype (ZMod n)] : Fintype.card (ZMod n) = n
 
ZMod.card: ∀ (n : ℕ) [inst : Fintype (ZMod n)], Fintype.card (ZMod n) = n
ZMod.card

-- example (z : ZMod 3) : 1 = 1 := by
--   cases z.val with
--   | zero => rfl
--   | succ n => rfl

-- example (q : Q₈) : Nat.repeat QuaternionGroup.f 3 q = 1 := by
--   simp only [QuaternionGroup.one_def, Nat.repeat]
--   cases q with
--   | a i => cases i.val with
--     | zero =>
--         rw (config := {occs := .pos {1} }) [QuaternionGroup.f]
--         done
--     | succ n => repeat { rw [QuaternionGroup.f] }
--     | _ => sorry
--   | _ => sorry
--   done

-- def φ : C₃ →* MulAut Q₈ where
--   toFun c := {
--       toFun := fun q => Nat.repeat QuaternionGroup.f c.val q, -- ^c.val,
--       invFun := fun q => Nat.repeat QuaternionGroup.f (c.val + 1) q, --^c.val,
--       left_inv := fun x => by
--         simp [Function.LeftInverse, QuaternionGroup.f]
--         done
--       right_inv := fun x => by simp [Function.RightInverse]
--       map_mul' := by simp [Function.LeftInverse, Function.RightInverse]
--   }
--   map_one' := sorry
--   map_mul' := sorry

-- #check Q₈ ⋊[φ] C₃

-- #check Q₈ ⋊[φ] C₃

-- https://en.wikipedia.org/wiki/Presentation_of_a_group
-- https://mathworld.wolfram.com/GroupPresentation.html
-- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Coxeter.20Groups
-- https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Group.20algebra.20over.20finite.20groups
-- https://encyclopediaofmath.org/wiki/Schur_index
-- https://en.wikipedia.org/wiki/Covering_groups_of_the_alternating_and_symmetric_groups
-- https://math.stackexchange.com/questions/4242277/number-of-schur-covering-groups
-- https://en.m.wikipedia.org/wiki/Tietze_transformations
-- https://mathworld.wolfram.com/GroupAlgebra.html
-- https://github.com/leanprover-community/mathlib4/commits/j-loreaux/generator/

PresentedGroup.{u_1} {α : Type u_1} (rels : Set (FreeGroup α)) : Type u_1
 
PresentedGroup: {α : Type u_1} → Set (FreeGroup α) → Type u_1
PresentedGroup

variable {
B: Type u_1
B : 
Type*: Type (u_1 + 1)
Type*} [
DecidableEq: Type u_1 → Type (max 0 u_1)
DecidableEq 
B: Type u_1
B] in
def 
demo: Type u_1
demo := 
PresentedGroup: {α : Type u_1} → Set (FreeGroup α) → Type u_1
PresentedGroup <| 
Set.range: {α ι : Type u_1} → (ι → α) → Set α
Set.range <| 
Function.uncurry: {α β φ : Type u_1} → (α → β → φ) → α × β → φ
Function.uncurry fun (
i: B
i 
j: B
j : 
B: Type u_1
B) => 
FreeGroup.of: {α : Type u_1} → α → FreeGroup α
FreeGroup.of 
i: B
i * 
FreeGroup.of: {α : Type u_1} → α → FreeGroup α
FreeGroup.of 
j: B
j

inductive 
generator: ℕ → Type
generator (
n: ℕ
n : 
ℕ: Type
ℕ)
  | 
a: {n : ℕ} → ZMod n → generator n
a : 
ZMod: ℕ → Type
ZMod 
n: ℕ
n → 
generator: ℕ → Type
generator 
n: ℕ
n
  | 
b: {n : ℕ} → ZMod n → generator n
b : 
ZMod: ℕ → Type
ZMod 
n: ℕ
n → 
generator: ℕ → Type
generator 
n: ℕ
n
  deriving 
DecidableEq: Sort u → Sort (max 1 u)
DecidableEq

def 
rel: generator n → generator n → FreeGroup (generator n)
rel : 
generator: ℕ → Type
generator 
n: ℕ
n → 
generator: ℕ → Type
generator 
n: ℕ
n → 
FreeGroup: Type → Type
FreeGroup (
generator: ℕ → Type
generator 
n: ℕ
n)
  | 
generator.a: {n : ℕ} → ZMod n → generator n
generator.a 
i: ZMod n
i, 
generator.a: {n : ℕ} → ZMod n → generator n
generator.a 
j: ZMod n
j => 
FreeGroup.of: {α : Type} → α → FreeGroup α
FreeGroup.of (
generator.a: {n : ℕ} → ZMod n → generator n
generator.a 
i: ZMod n
i) * 
FreeGroup.of: {α : Type} → α → FreeGroup α
FreeGroup.of (
generator.a: {n : ℕ} → ZMod n → generator n
generator.a 
j: ZMod n
j)
  | 
generator.b: {n : ℕ} → ZMod n → generator n
generator.b 
i: ZMod n
i, 
generator.b: {n : ℕ} → ZMod n → generator n
generator.b 
j: ZMod n
j => 
FreeGroup.of: {α : Type} → α → FreeGroup α
FreeGroup.of (
generator.b: {n : ℕ} → ZMod n → generator n
generator.b 
i: ZMod n
i) * 
FreeGroup.of: {α : Type} → α → FreeGroup α
FreeGroup.of (
generator.b: {n : ℕ} → ZMod n → generator n
generator.b 
j: ZMod n
j)
  | 
generator.a: {n : ℕ} → ZMod n → generator n
generator.a 
i: ZMod n
i, 
generator.b: {n : ℕ} → ZMod n → generator n
generator.b 
j: ZMod n
j => (
FreeGroup.of: {α : Type} → α → FreeGroup α
FreeGroup.of (
generator.a: {n : ℕ} → ZMod n → generator n
generator.a 
j: ZMod n
j) * 
FreeGroup.of: {α : Type} → α → FreeGroup α
FreeGroup.of (
generator.b: {n : ℕ} → ZMod n → generator n
generator.b 
i: ZMod n
i))^
n: ℕ
n
  | 
generator.b: {n : ℕ} → ZMod n → generator n
generator.b 
i: ZMod n
i, 
generator.a: {n : ℕ} → ZMod n → generator n
generator.a 
j: ZMod n
j => (
FreeGroup.of: {α : Type} → α → FreeGroup α
FreeGroup.of (
generator.b: {n : ℕ} → ZMod n → generator n
generator.b 
j: ZMod n
j) * 
FreeGroup.of: {α : Type} → α → FreeGroup α
FreeGroup.of (
generator.a: {n : ℕ} → ZMod n → generator n
generator.a 
i: ZMod n
i))^
n: ℕ
n


rel (n : ℕ) : generator n → generator n → FreeGroup (generator n)
 
rel: (n : ℕ) → generator n → generator n → FreeGroup (generator n)
rel

The presentation of the Dihedral group which makes it a Coxeter group is ⟨a, b | a^2 = 1, b^2 = 1, (a * b)^n = 1⟩

def 
DihedralPresentedGroup: {_i : ZMod n} → Type
DihedralPresentedGroup {
_i: ZMod n
_i : 
ZMod: ℕ → Type
ZMod 
n: ℕ
n} := 
PresentedGroup: {α : Type} → Set (FreeGroup α) → Type
PresentedGroup <| 
Set.range: {α ι : Type} → (ι → α) → Set α
Set.range <| 
Function.uncurry: {α β φ : Type} → (α → β → φ) → α × β → φ
Function.uncurry <| 
rel: (n : ℕ) → generator n → generator n → FreeGroup (generator n)
rel 
n: ℕ
n

namespace DihedralPresentedGroup

inductive 
pre: ℕ → Type
pre (
n: ℕ
n : 
ℕ: Type
ℕ)
  | 
a: {n : ℕ} → ZMod n → pre n
a : 
ZMod: ℕ → Type
ZMod 
n: ℕ
n → 
pre: ℕ → Type
pre 
n: ℕ
n
  | 
b: {n : ℕ} → ZMod n → pre n
b : 
ZMod: ℕ → Type
ZMod 
n: ℕ
n → 
pre: ℕ → Type
pre 
n: ℕ
n
  deriving 
DecidableEq: Sort u → Sort (max 1 u)
DecidableEq


1 : FreeGroup (pre n)
 (
1: FreeGroup (pre n)
1 : 
FreeGroup: Type → Type
FreeGroup (
pre: ℕ → Type
pre 
n: ℕ
n))

The presentation of the Dihedral group which makes it a Coxeter group is ⟨a, b | a^2 = 1, b^2 = 1, (a * b)^n = 1⟩

def 
rel: {i : ZMod n} → Set (FreeGroup (pre n))
rel {
i: ZMod n
i : 
ZMod: ℕ → Type
ZMod 
n: ℕ
n} : 
Set: Type → Type
Set (
FreeGroup: Type → Type
FreeGroup (
pre: ℕ → Type
pre 
n: ℕ
n)) :=
  {
FreeGroup.of: {α : Type} → α → FreeGroup α
FreeGroup.of (
pre.a: {n : ℕ} → ZMod n → pre n
pre.a 
i: ZMod n
i)^
2: ℕ
2} ∪
  {
FreeGroup.of: {α : Type} → α → FreeGroup α
FreeGroup.of (
pre.b: {n : ℕ} → ZMod n → pre n
pre.b 
i: ZMod n
i)^
2: ℕ
2} ∪
  {(
FreeGroup.of: {α : Type} → α → FreeGroup α
FreeGroup.of (
pre.a: {n : ℕ} → ZMod n → pre n
pre.a 
i: ZMod n
i) * 
FreeGroup.of: {α : Type} → α → FreeGroup α
FreeGroup.of (
pre.b: {n : ℕ} → ZMod n → pre n
pre.b 
i: ZMod n
i)) ^ 
n: ℕ
n}

abbrev 
DihedralPresentedGroup': {i : ZMod n} → Type
DihedralPresentedGroup' {
i: ZMod n
i : 
ZMod: ℕ → Type
ZMod 
n: ℕ
n} := 
PresentedGroup: {α : Type} → Set (FreeGroup α) → Type
PresentedGroup <| @
rel: (n : ℕ) → {i : ZMod n} → Set (FreeGroup (pre n))
rel 
n: ℕ
n 
i: ZMod n
i

end DihedralPresentedGroup

namespace PresentedQuaternionGroup

-- variable {X : Type*} [DecidableEq X]

inductive 
pre: Type
pre
  | 
x: pre
x : 
pre: Type
pre
  | 
y: pre
y : 
pre: Type
pre
  deriving 
DecidableEq: Sort u → Sort (max 1 u)
DecidableEq

inductive 
rel: {n : ℕ} → FreeGroup pre → FreeGroup pre → Prop
rel {
n: ℕ
n : 
ℕ: Type
ℕ} : 
FreeGroup: Type → Type
FreeGroup 
pre: Type
pre → 
FreeGroup: Type → Type
FreeGroup 
pre: Type
pre → 
Prop: Type
Prop
| 
cond1: ∀ {n : ℕ}, rel (FreeGroup.of pre.x ^ n) (FreeGroup.of pre.y ^ 2)
cond1 : 
rel: {n : ℕ} → FreeGroup pre → FreeGroup pre → Prop
rel ((
FreeGroup.of: {α : Type} → α → FreeGroup α
FreeGroup.of 
pre.x: pre
pre.x)^
n: ℕ
n) ((
FreeGroup.of: {α : Type} → α → FreeGroup α
FreeGroup.of 
pre.y: pre
pre.y)^
2: ℕ
2)
| 
cond2: ∀ {n : ℕ}, rel ((FreeGroup.of pre.y)⁻¹ * FreeGroup.of pre.x * FreeGroup.of pre.y) (FreeGroup.of pre.x)⁻¹
cond2 : 
rel: {n : ℕ} → FreeGroup pre → FreeGroup pre → Prop
rel ((
FreeGroup.of: {α : Type} → α → FreeGroup α
FreeGroup.of 
pre.y: pre
pre.y)⁻¹ * (
FreeGroup.of: {α : Type} → α → FreeGroup α
FreeGroup.of 
pre.x: pre
pre.x) * (
FreeGroup.of: {α : Type} → α → FreeGroup α
FreeGroup.of 
pre.y: pre
pre.y)) ((
FreeGroup.of: {α : Type} → α → FreeGroup α
FreeGroup.of 
pre.x: pre
pre.x)⁻¹)

end PresentedQuaternionGroup

namespace C

-- variable {X : Type*} [DecidableEq X]

inductive 
pre: Type
pre
  | 
a: pre
a : 
pre: Type
pre
  deriving 
DecidableEq: Sort u → Sort (max 1 u)
DecidableEq

def 
rel: Set (FreeGroup pre)
rel := {
a: FreeGroup pre
a : 
FreeGroup: Type → Type
FreeGroup 
pre: Type
pre| 
a: FreeGroup pre
a^
n: ℕ
n = 
1: FreeGroup pre
1}

end C

abbrev 
C: ℕ → Type
C (
n: ℕ
n : 
ℕ: Type
ℕ) := 
PresentedGroup: {α : Type} → Set (FreeGroup α) → Type
PresentedGroup <| 
C.rel: ℕ → Set (FreeGroup C.pre)
C.rel 
n: ℕ
n


PresentedGroup.instGroup (C.rel 3)


namespace D

inductive 
pre: Type
pre
  | 
x: pre
x : 
pre: Type
pre
  | 
y: pre
y : 
pre: Type
pre
  deriving 
DecidableEq: Sort u → Sort (max 1 u)
DecidableEq

def 
x: FreeGroup pre
x := 
FreeGroup.of: {α : Type} → α → FreeGroup α
FreeGroup.of 
pre.x: pre
pre.x
def 
y: FreeGroup pre
y := 
FreeGroup.of: {α : Type} → α → FreeGroup α
FreeGroup.of 
pre.y: pre
pre.y

def 
rel: Set (FreeGroup pre)
rel : 
Set: Type → Type
Set (
FreeGroup: Type → Type
FreeGroup 
pre: Type
pre) := {
x: FreeGroup pre
x^
n: ℕ
n} ∪ {
y: FreeGroup pre
y^
2: ℕ
2} ∪ {(
x: FreeGroup pre
x * 
y: FreeGroup pre
y)^
2: ℕ
2}

end D

abbrev 
D: ℕ → Type
D (
n: ℕ
n : 
ℕ: Type
ℕ) := 
PresentedGroup: {α : Type} → Set (FreeGroup α) → Type
PresentedGroup <| 
D.rel: ℕ → Set (FreeGroup D.pre)
D.rel 
n: ℕ
n

namespace De

variable {
X: Type u_1
X : 
Type*: Type (u_1 + 1)
Type*} [
DecidableEq: Type u_1 → Type (max 0 u_1)
DecidableEq 
X: Type u_1
X]

def 
rel: ℕ → {X : Type u_1} → {x y : FreeGroup X} → Set (FreeGroup X)
rel {
x: FreeGroup X
x 
y: FreeGroup X
y : 
FreeGroup: Type u_1 → Type u_1
FreeGroup 
X: Type u_1
X} : 
Set: Type u_1 → Type u_1
Set (
FreeGroup: Type u_1 → Type u_1
FreeGroup 
X: Type u_1
X) := {
x: FreeGroup X
x^
n: ℕ
n} ∪ {
y: FreeGroup X
y^
2: ℕ
2} ∪ {(
x: FreeGroup X
x * 
y: FreeGroup X
y)^
2: ℕ
2}

end De

def 
De: ℕ → Type
De (
n: ℕ
n : 
ℕ: Type
ℕ) := 
PresentedGroup: {α : Type} → Set (FreeGroup α) → Type
PresentedGroup <| @
De.rel: ℕ → {X : Type} → {x y : FreeGroup X} → Set (FreeGroup X)
De.rel 
n: ℕ
n 
D.pre: Type
D.pre 
D.x: FreeGroup D.pre
D.x 
D.y: FreeGroup D.pre
D.y

namespace Q

inductive 
pre: Type
pre
  | 
x: pre
x : 
pre: Type
pre
  | 
y: pre
y : 
pre: Type
pre
  deriving 
DecidableEq: Sort u → Sort (max 1 u)
DecidableEq

def 
x: FreeGroup pre
x := 
FreeGroup.of: {α : Type} → α → FreeGroup α
FreeGroup.of 
pre.x: pre
pre.x
def 
y: FreeGroup pre
y := 
FreeGroup.of: {α : Type} → α → FreeGroup α
FreeGroup.of 
pre.y: pre
pre.y

def 
rel: Set (FreeGroup pre)
rel : 
Set: Type → Type
Set (
FreeGroup: Type → Type
FreeGroup 
pre: Type
pre) := {
x: FreeGroup pre
x^
4: ℕ
4} ∪ {
y: FreeGroup pre
y^
4: ℕ
4} ∪ {
y: FreeGroup pre
y⁻¹ * 
x: FreeGroup pre
x * 
y: FreeGroup pre
y * 
x: FreeGroup pre
x}

end Q

abbrev 
Q: Type
Q := 
PresentedGroup: {α : Type} → Set (FreeGroup α) → Type
PresentedGroup <| 
Q.rel: Set (FreeGroup Q.pre)
Q.rel


PresentedGroup.instGroup Q.rel


def 
Warning: declaration uses 'sorry'
Warning: declaration uses 'sorry'
Warning: declaration uses 'sorry'
Warning: declaration uses 'sorry'
Warning: declaration uses 'sorry'
 : 
C: ℕ → Type
C 
3: ℕ
3 →* 
MulAut: (M : Type) → [inst : Mul M] → Type
MulAut 
Q: Type
Q where
  toFun 
c: C 3
c := {
      toFun := fun 
q: Q
q => 
sorry: Q
sorry,
      invFun := fun 
q: Q
q => 
sorry: Q
sorry,
      left_inv := fun 
x: Q
x => 
Goals accomplished! 🐙
 
p: ℕ
inst✝⁶: Fact (Nat.Prime p)
F: Type uF
inst✝⁵: Field F
ι: Type uι
inst✝⁴: Finite ι
inst✝³: LT ι
R: Type uR
inst✝²: Ring R
G, H: Type uG
inst✝¹: Group G
inst✝: Group H
K, L: Subgroup G
n: ℕ
c: C 3
x: Q
sorryAx Q = x
; 
Goals accomplished! 🐙

      right_inv := fun 
x: Q
x => 
Goals accomplished! 🐙
 
p: ℕ
inst✝⁶: Fact (Nat.Prime p)
F: Type uF
inst✝⁵: Field F
ι: Type uι
inst✝⁴: Finite ι
inst✝³: LT ι
R: Type uR
inst✝²: Ring R
G, H: Type uG
inst✝¹: Group G
inst✝: Group H
K, L: Subgroup G
n: ℕ
c: C 3
x: Q
sorryAx Q = x
; 
Goals accomplished! 🐙

      map_mul' := 
Goals accomplished! 🐙
 
p: ℕ
inst✝⁶: Fact (Nat.Prime p)
F: Type uF
inst✝⁵: Field F
ι: Type uι
inst✝⁴: Finite ι
inst✝³: LT ι
R: Type uR
inst✝²: Ring R
G, H: Type uG
inst✝¹: Group G
inst✝: Group H
K, L: Subgroup G
n: ℕ
c: C 3
sorryAx Q = 1
; 
Goals accomplished! 🐙

  }
  map_one' := 
sorry: (fun c => { toFun := fun q => sorryAx Q, invFun := fun q => sorryAx Q, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ })
    1 =
  1
sorry
  map_mul' := 
sorry: ∀ (x y : C 3),
  {
          toFun := fun c =>
            { toFun := fun q => sorryAx Q, invFun := fun q => sorryAx Q, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ },
          map_one' := ⋯ }.toFun
      (x * y) =
    {
            toFun := fun c =>
              { toFun := fun q => sorryAx Q, invFun := fun q => sorryAx Q, left_inv := ⋯, right_inv := ⋯,
                map_mul' := ⋯ },
            map_one' := ⋯ }.toFun
        x *
      {
            toFun := fun c =>
              { toFun := fun q => sorryAx Q, invFun := fun q => sorryAx Q, left_inv := ⋯, right_inv := ⋯,
                map_mul' := ⋯ },
            map_one' := ⋯ }.toFun
        y
sorry


Q ⋊[φ] C 3 : Type
 
Q: Type
Q ⋊[
φ: C 3 →* MulAut Q
φ] 
C: ℕ → Type
C 
3: ℕ
3


SemidirectProduct.instGroup


namespace BT

inductive 
pre: Type
pre
  | 
e: pre
e : 
pre: Type
pre
  | 
ne: pre
ne : 
pre: Type
pre
  | 
i: pre
i : 
pre: Type
pre
  | 
j: pre
j : 
pre: Type
pre
  | 
k: pre
k : 
pre: Type
pre
  | 
f: pre
f : 
pre: Type
pre
  | 
g: pre
g : 
pre: Type
pre
  deriving 
DecidableEq: Sort u → Sort (max 1 u)
DecidableEq

def 
e: FreeGroup pre
e := 
FreeGroup.of: {α : Type} → α → FreeGroup α
FreeGroup.of 
pre.e: pre
pre.e
def 
ne: FreeGroup pre
ne := 
FreeGroup.of: {α : Type} → α → FreeGroup α
FreeGroup.of 
pre.ne: pre
pre.ne
def 
i: FreeGroup pre
i := 
FreeGroup.of: {α : Type} → α → FreeGroup α
FreeGroup.of 
pre.i: pre
pre.i
def 
j: FreeGroup pre
j := 
FreeGroup.of: {α : Type} → α → FreeGroup α
FreeGroup.of 
pre.j: pre
pre.j
def 
k: FreeGroup pre
k := 
FreeGroup.of: {α : Type} → α → FreeGroup α
FreeGroup.of 
pre.k: pre
pre.k
def 
f: FreeGroup pre
f := 
FreeGroup.of: {α : Type} → α → FreeGroup α
FreeGroup.of 
pre.f: pre
pre.f
def 
g: FreeGroup pre
g := 
FreeGroup.of: {α : Type} → α → FreeGroup α
FreeGroup.of 
pre.g: pre
pre.g

def 
rel: Set (FreeGroup pre)
rel : 
Set: Type → Type
Set (
FreeGroup: Type → Type
FreeGroup 
pre: Type
pre) :=
  {
e: FreeGroup pre
e} ∪ {
ne: FreeGroup pre
ne^
2: ℕ
2} ∪ {
i: FreeGroup pre
i^
4: ℕ
4} ∪ {
j: FreeGroup pre
j^
4: ℕ
4} ∪ {
i: FreeGroup pre
i * 
j: FreeGroup pre
j * 
k: FreeGroup pre
k} ∪
  {
f: FreeGroup pre
f^
3: ℕ
3} ∪ {
g: FreeGroup pre
g^
3: ℕ
3} ∪ {
f: FreeGroup pre
f * 
g: FreeGroup pre
g} ∪ {
f: FreeGroup pre
f⁻¹ * 
i: FreeGroup pre
i * 
f: FreeGroup pre
f * 
j: FreeGroup pre
j⁻¹} ∪ {
f: FreeGroup pre
f⁻¹ * 
j: FreeGroup pre
j * 
f: FreeGroup pre
f * 
k: FreeGroup pre
k⁻¹}

end BT

-- example (a b: BT) [Group BT] : a^6 = 1 := by
--   done

abbrev 
BT: Type
BT := 
PresentedGroup: {α : Type} → Set (FreeGroup α) → Type
PresentedGroup <| 
BT.rel: Set (FreeGroup BT.pre)
BT.rel

-- namespace TT

-- inductive pre
-- | ofQ :  FreeGroup Q.pre → pre
-- | ofC :  FreeGroup C.pre → pre

-- def relQ := { FreeGroup.of <| pre.ofQ q | q ∈ Q.rel }
-- def relC := { FreeGroup.of <| pre.ofC c | c ∈ C.rel 3 }

-- def QC := FreeGroup <| Q.pre × C.pre

-- def rel : Set (FreeGroup pre) :=
--   relQ ∪ relC

-- end TT

-- https://people.maths.bris.ac.uk/~matyd/GroupNames/1/e5/C3byQ8.html#s1
-- https://people.maths.bris.ac.uk/~matyd/GroupNames/1/SL(2,3).html
-- https://en.wikipedia.org/wiki/Direct_product_of_groups#Presentations
abbrev 
TT: Type
TT := 
Q: Type
Q × 
C: ℕ → Type
C 
3: ℕ
3


Prod.instGroup



Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)
 
Prod: Type u → Type v → Type (max u v)
Prod


Prod.instGroup.{u_1, u_2} {G : Type u_1} {H : Type u_2} [Group G] [Group H] : Group (G × H)
 
Prod.instGroup: {G : Type u_1} → {H : Type u_2} → [inst : Group G] → [inst : Group H] → Group (G × H)
Prod.instGroup


MulHom.{u_10, u_11} (M : Type u_10) (N : Type u_11) [Mul M] [Mul N] : Type (max u_10 u_11)
 
MulHom: (M : Type u_10) → (N : Type u_11) → [inst : Mul M] → [inst : Mul N] → Type (max u_10 u_11)
MulHom

-- free product of groups

Monoid.Coprod.{u_1, u_2} (M : Type u_1) (N : Type u_2) [MulOneClass M] [MulOneClass N] : Type (max u_1 u_2)
 
Monoid.Coprod: (M : Type u_1) → (N : Type u_2) → [inst : MulOneClass M] → [inst : MulOneClass N] → Type (max u_1 u_2)
Monoid.Coprod

open Monoid.Coprod


Q ∗ C 3 : Type
 
Q: Type
Q ∗ 
C: ℕ → Type
C 
3: ℕ
3

namespace BT

def 
of: pre → PresentedGroup rel
of := @
PresentedGroup.of: {α : Type} → {rels : Set (FreeGroup α)} → α → PresentedGroup rels
PresentedGroup.of 
pre: Type
pre 
rel: Set (FreeGroup pre)
rel

def 
k': PresentedGroup rel
k' := 
BT.of: pre → PresentedGroup rel
BT.of 
pre.k: pre
pre.k
def 
f': PresentedGroup rel
f' := 
BT.of: pre → PresentedGroup rel
BT.of 
pre.f: pre
pre.f
def 
i': PresentedGroup rel
i' := 
BT.of: pre → PresentedGroup rel
BT.of 
pre.i: pre
pre.i

-- example : f'⁻¹ * k' * f' = i' := by
--   simp [f', k', i', BT.of, BT.rel] --, pre.k, pre.f, pre.i]
--   have h : i'^4 = BT.of pre.e := by
--     simp [i', BT.of, BT.rel]
--     done
--     done
--   done
--   done
--   done
--   done

end BT

-- TODO Tietze transformations
-- https://math.stackexchange.com/questions/4273898/proving-an-isomorphism-via-generators