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.CategoryTheory.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.DirectSum.Basis
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_3, u_4} (R : Type u_1) {S : Type u_3} (M : Type u_4) [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_3} →
    (M : Type u_4) →
      [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 : Type u} [Group G] (A : Action V G) :
  G →* CategoryTheory.Aut A.V
 
Action.ρAut: {V : Type (u + 1)} →
  [inst : CategoryTheory.LargeCategory V] →
    {G : Type u} → [inst_1 : Group G] → (A : Action V G) → G →* CategoryTheory.Aut A.V
Action.ρAut


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


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


isCyclic_of_prime_card.{u_1} {α : Type u_1} [Group α] {p : ℕ} [hp : Fact (Nat.Prime p)] (h : Nat.card α = p) :
  IsCyclic α
 
isCyclic_of_prime_card: ∀ {α : Type u_1} [inst : Group α] {p : ℕ} [hp : Fact (Nat.Prime p)], Nat.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.EuclideanDomain.Field
import Mathlib.Algebra.Group.Action.Defs
import Mathlib.Algebra.Group.End
import Mathlib.Data.Finsupp.Defs
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


Group.inv_mul_cancel.{u} {G : Type u} [self : Group G] (a : G) : a⁻¹ * a = 1
 
Group.inv_mul_cancel: ∀ {G : Type u} [self : Group G] (a : G), a⁻¹ * a = 1
Group.inv_mul_cancel


Subgroup.{u_3} (G : Type u_3) [Group G] : Type u_3
 
Subgroup: (G : Type u_3) → [inst : Group G] → Type u_3
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 : Type u} [Monoid G] (M N : Action V G) : Type u
 
Action.Hom: {V : Type (u + 1)} →
  [inst : CategoryTheory.LargeCategory V] → {G : Type u} → [inst_1 : Monoid G] → 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) [hN : N.Normal] :
  ↥H ⧸ N.subgroupOf H ≃* ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N)
 
QuotientGroup.quotientInfEquivProdNormalQuotient: {G : Type u} →
  [inst : Group G] → (H N : Subgroup G) → [hN : 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, u_3, u_5} {R : Type u} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M]
  [Nontrivial R] {ι : Type u_5} [Module.Finite R M] (b : Basis ι R M) : Finite ι
 
Module.Finite.finite_basis: ∀ {R : Type u} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Nontrivial R] {ι : Type u_5} [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) [Semiring R] [StrongRankCondition R] [AddCommMonoid 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 : Semiring R] →
      [inst_1 : StrongRankCondition R] →
        [inst_2 : AddCommMonoid 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.linearCombination.{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.linearCombination: {α : 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.linearCombination 

/- `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_10, u_11, u_12} {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M]
  [Module R M] (b : Basis ι R M) (i : ι) : M →ₗ[R] R
 
Basis.coord: {ι : Type u_10} →
  {R : Type u_11} →
    {M : Type u_12} →
      [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_1, u_2, u_3} (R : Type u_1) [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_1) [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


LinearMap.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
 
LinearMap.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
LinearMap.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) [Semiring R] [StrongRankCondition R] [AddCommMonoid M]
  [Module R M] [Module.Free R M] [AddCommMonoid 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 : Semiring R] →
      [inst_1 : StrongRankCondition R] →
        [inst_2 : AddCommMonoid M] →
          [inst_3 : Module R M] →
            [inst_4 : Module.Free R M] →
              [inst_5 : AddCommMonoid 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_4} {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] :
  Semiring (Module.End R M)
 
Module.End.semiring: {R : Type u_1} →
  {M : Type u_4} → [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_3, u_4} (R : Type u_1) {S : Type u_3} (M : Type u_4) [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_3} →
    (M : Type u_4) →
      [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_3, u_4} (R : Type u_1) {S : Type u_3} (M : Type u_4) [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_3} →
    (M : Type u_4) →
      [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 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 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} [CommSemiring R] {n : Type u_2} [DecidableEq n] {M : Type u_3}
  [AddCommMonoid 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 : CommSemiring R] →
    {n : Type u_2} →
      [inst_1 : DecidableEq n] →
        {M : Type u_3} →
          [inst_2 : AddCommMonoid 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) : iSupIndep 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), iSupIndep 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, ↑(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, ↑(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) ↔ IsIdempotentElem 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) ↔ IsIdempotentElem 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 ≃ₗ[k] 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 ≃ₗ[k] 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.Functor.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.Functor.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.Functor.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_12, u_13} (M : Type u_12) (A : Type u_13) [Monoid M] [AddMonoid A] : Type (max u_12 u_13)
 
DistribMulAction: (M : Type u_12) → (A : Type u_13) → [inst : Monoid M] → [inst : AddMonoid A] → Type (max u_12 u_13)
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 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'
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
sorry = 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
sorry = 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
sorry = 1
; 
Goals accomplished! 🐙

  }
  map_one' := 
sorry: (fun c => { toFun := fun q => sorry, invFun := fun q => sorry, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }) 1 = 1
sorry
  map_mul' := 
sorry: ∀ (x y : C 3),
  {
          toFun := fun c =>
            { toFun := fun q => sorry, invFun := fun q => sorry, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ },
          map_one' := ⋯ }.toFun
      (x * y) =
    {
            toFun := fun c =>
              { toFun := fun q => sorry, invFun := fun q => sorry, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ },
            map_one' := ⋯ }.toFun
        x *
      {
            toFun := fun c =>
              { toFun := fun q => sorry, invFun := fun q => sorry, 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