mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → F
hv : v ≠ 0
A : SpecialLinearGroup ι F
hA : A ∈ lineStab (F ∙ v)
⊢ A • v = v

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
W : Type u_3
X : Type u_4
inst✝³ : AddCommGroup W
inst✝² : Module R W
inst✝¹ : AddCommGroup X
inst✝ : Module R X
e : V ≃ₗ[R] W
g : SpecialLinearGroup R W
⊢ (fun a ↦ ↑a) ((fun f ↦ ⟨e.symm ≪≫ₗ ↑f ≪≫ₗ e, ⋯⟩) ((fun g ↦ ⟨e ≪≫ₗ ↑g ≪≫ₗ e.symm, ⋯⟩) g)) = (fun a ↦ ↑a) g

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
W : Type u_3
X : Type u_4
inst✝³ : AddCommGroup W
inst✝² : Module R W
inst✝¹ : AddCommGroup X
inst✝ : Module R X
e : V ≃ₗ[R] W
f g : SpecialLinearGroup R V
⊢ (fun a ↦ ↑a) ⟨e.symm ≪≫ₗ ↑(f * g) ≪≫ₗ e, ⋯⟩ = (fun a ↦ ↑a) (⟨e.symm ≪≫ₗ ↑f ≪≫ₗ e, ⋯⟩ * ⟨e.symm ≪≫ₗ ↑g ≪≫ₗ e, ⋯⟩)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
W : Type u_3
X : Type u_4
inst✝³ : AddCommGroup W
inst✝² : Module R W
inst✝¹ : AddCommGroup X
inst✝ : Module R X
e : V ≃ₗ[R] W
f : W ≃ₗ[R] X
⊢ (congr_linearEquiv e).trans (congr_linearEquiv f) = congr_linearEquiv (e ≪≫ₗ f)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
⊢ congr_linearEquiv (LinearEquiv.refl R V) = MulEquiv.refl (SpecialLinearGroup R V)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
b : Module.Basis n R V
A : SpecialLinearGroup n R
⊢ LinearEquiv.det (toLin' A) = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
b : Module.Basis n R V
u : _root_.SpecialLinearGroup R (n → R)
⊢ (LinearMap.toMatrix' ↑↑u).det = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
b : Module.Basis n R V
A : SpecialLinearGroup n R
⊢ (fun a ↦ ↑a) ((fun u ↦ ⟨LinearMap.toMatrix' ↑↑u, ⋯⟩) ((fun A ↦ ⟨toLin' A, ⋯⟩) A)) = (fun a ↦ ↑a) A

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
b : Module.Basis n R V
u : _root_.SpecialLinearGroup R (n → R)
⊢ (fun a ↦ ↑a) ((fun A ↦ ⟨toLin' A, ⋯⟩) ((fun u ↦ ⟨LinearMap.toMatrix' ↑↑u, ⋯⟩) u)) = (fun a ↦ ↑a) u

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
b : Module.Basis n R V
A B : SpecialLinearGroup n R
⊢ (fun a ↦ ↑a) ⟨toLin' (A * B), ⋯⟩ = (fun a ↦ ↑a) (⟨toLin' A, ⋯⟩ * ⟨toLin' B, ⋯⟩)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Field K
inst✝ : Module K V
this✝¹ : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
a : Kˣ
this✝ : LinearIndepOn K id {D.rep, D'.rep}
s : Set V := ⋯.extend ⋯
b : Module.Basis (↑s) K V := Module.Basis.extend this✝
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
this : (b.repr D'.rep) ⟨D.rep, hD_mem⟩ = 0
⊢ D'.rep = D'.rep + (b.repr D'.rep) ⟨D.rep, hD_mem⟩ • (↑a - 1) • b ⟨D.rep, hD_mem⟩

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
h : Module.finrank R V ≤ 1
a✝ : Nontrivial R
b : Module.Basis (Module.Free.ChooseBasisIndex R V) R V := Module.Free.chooseBasis R V
⊢ Subsingleton (Module.Free.ChooseBasisIndex R V)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
h : Module.finrank R V ≤ 1
a✝ : Nontrivial R
b : Module.Basis (Module.Free.ChooseBasisIndex R V) R V := Module.Free.chooseBasis R V
this : Subsingleton (Module.Free.ChooseBasisIndex R V)
⊢ Subsingleton ↥(Subgroup.center (Matrix.SpecialLinearGroup (Module.Free.ChooseBasisIndex R V) R))

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → F
hv : v ≠ 0
A B : SpecialLinearGroup ι F
hA : A ∈ lineStab (F ∙ v)
hB : B ∈ lineStab (F ∙ v)
⊢ A * B = B * A

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → F
hv : v ≠ 0
x✝¹ x✝ : ↥(lineStab (F ∙ v))
A : SpecialLinearGroup ι F
hA : A ∈ lineStab (F ∙ v)
B : SpecialLinearGroup ι F
hB : B ∈ lineStab (F ∙ v)
⊢ ⟨A, hA⟩ * ⟨B, hB⟩ = ⟨B, hB⟩ * ⟨A, hA⟩

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
h : Module.finrank R V ≤ 1
⊢ Subgroup.center (SpecialLinearGroup R V) = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g : SpecialLinearGroup R V
hR : Nontrivial R
b : Module.Basis (Module.Free.ChooseBasisIndex R V) R V := Module.Free.chooseBasis R V
this✝ : Fintype (Module.Free.ChooseBasisIndex R V) := Module.Free.ChooseBasisIndex.fintype R V
e : SpecialLinearGroup R V ≃* Matrix.SpecialLinearGroup (Module.Free.ChooseBasisIndex R V) R :=
  (Matrix.SpecialLinearGroup.toLin_equiv b).symm
r : R
hr : r ^ Fintype.card (Module.Free.ChooseBasisIndex R V) = 1
this : ↑((Matrix.SpecialLinearGroup.toLin_equiv b).symm g) = Matrix.of fun i j ↦ (b.repr ((fun x ↦ ↑g x) (b j))) i
⊢ (Matrix.diagonal fun x ↦ r) = ↑((Matrix.SpecialLinearGroup.toLin_equiv b).symm g) ↔ ↑↑g = r • LinearMap.id

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g : SpecialLinearGroup R V
⊢ g ∈ Subgroup.center (SpecialLinearGroup R V) ↔ ∃ r, r ^ Module.finrank R V = 1 ∧ ↑↑g = r • LinearMap.id

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g : SpecialLinearGroup R V
hg : g ∈ Subgroup.center (SpecialLinearGroup R V)
x : V
⊢ ↑↑g x = ⋯.choose • x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
⊢ IsUnit (LinearMap.det (↑↑r • LinearMap.id))

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Field K
inst✝ : Module K V
this : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : D ≠ D'
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : ¬FiniteDimensional K V
⊢ LinearEquiv.det g = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Basis

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
g : ι → M
l : ι →₀ R
⊢ ∀ i ∈ l.support, 0 • (⇑Q ∘ g) i = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Field K
inst✝ : Module K V
⊢ IsMultiplyPretransitive (SpecialLinearGroup K V) (ℙ K V) 2

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Basis

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
g : ι → M
l : ι →₀ R
⊢ ∀ i ∈ l.support.sym2, 0 • (polarSym2 ⇑Q ∘ Sym2.map g) i = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Field K
inst✝² : Module K V
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
φ : SpecialLinearGroup K (ι → K) →* Matrix.SpecialLinearGroup ι K :=
  Matrix.SpecialLinearGroup.toLin'_equiv.symm.toMonoidHom
g : SpecialLinearGroup K (ι → K)
D : ℙ K (ι → K)
⊢ id (g • D) = φ g • id D

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Basis

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
g : ι → M
l : ι →₀ R
⊢ Q ((linearCombination R g) l) =
    (linearCombination R (polarSym2 ⇑Q ∘ Sym2.map g)) l.sym2Mul - (linearCombination R (⇑Q ∘ g)) (l * l)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Basis

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
⊢ (linearCombination R (polarSym2 ⇑Q ∘ Sym2.map ⇑bm)) (bm.repr x).sym2Mul -
      (linearCombination R (⇑Q ∘ ⇑bm)) (bm.repr x * bm.repr x) =
    Q x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
⊢ LinearEquiv.det (LinearMap.equivOfIsUnitDet ⋯) = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : Matrix.SpecialLinearGroup ι K
hm : ∀ (x : ℙ K (ι → K)), m • x = x
f : (ι → K) →ₗ[K] ι → K := ↑(Matrix.SpecialLinearGroup.toLin' m)
hf : f = ↑(Matrix.SpecialLinearGroup.toLin' m)
v : ι → K
⊢ ¬LinearIndependent K ![v, f v]

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : Matrix.SpecialLinearGroup ι K
hm : ∀ (x : ℙ K (ι → K)), m • x = x
f : (ι → K) →ₗ[K] ι → K := ↑(Matrix.SpecialLinearGroup.toLin' m)
hf : f = ↑(Matrix.SpecialLinearGroup.toLin' m)
a : K
ha : f = a • 1
⊢ ↑m = LinearMap.toMatrix' f

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Basis

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : DecidableEq ι
Q : QuadraticMap R M N
g : ι → M
l : ι →₀ R
⊢ ∀ i ∈ l.support, 0 • (⇑Q ∘ g) i = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : Matrix.SpecialLinearGroup ι K
hm : ∀ (x : ℙ K (ι → K)), m • x = x
f : (ι → K) →ₗ[K] ι → K := ↑(Matrix.SpecialLinearGroup.toLin' m)
hf : f = ↑(Matrix.SpecialLinearGroup.toLin' m)
a : K
ha : f = a • 1
hscalar : ↑m = (Matrix.scalar ι) a
⊢ a ^ Fintype.card ι = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ (toPermHom (Matrix.SpecialLinearGroup ι K) (ℙ K (ι → K))).ker = Subgroup.center (Matrix.SpecialLinearGroup ι K)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Basis

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : DecidableEq ι
Q : QuadraticMap R M N
g : ι → M
l : ι →₀ R
⊢ Q ((linearCombination R g) l) =
    (linearCombination R (⇑Q ∘ g)) (l * l) +
      ∑ p ∈ l.support.sym2 with ¬p.IsDiag, (Sym2.map (⇑l) p).mul • polarSym2 (⇑Q) (Sym2.map g p)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
⊢ ⟨LinearMap.equivOfIsUnitDet ⋯, ⋯⟩ ∈ Subgroup.center (SpecialLinearGroup R V)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ Function.Injective ⇑PSLAction.toPermHom

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Basis

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : DecidableEq ι
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
⊢ (linearCombination R (⇑Q ∘ ⇑bm)) (bm.repr x * bm.repr x) +
      ∑ p ∈ (bm.repr x).support.sym2 with ¬p.IsDiag,
        (Sym2.map (⇑(bm.repr x)) p).mul • polarSym2 (⇑Q) (Sym2.map (⇑bm) p) =
    Q x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Field K
inst✝² : Module K V
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : Matrix.ProjectiveSpecialLinearGroup ι K
hg : ∀ (a : ℙ K (ι → K)), g • a = a
x : ℙ K (ι → K)
⊢ (PSLAction.toPermHom g) x = (PSLAction.toPermHom 1) x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Basis

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
i j : ι
⊢ ((Q.toBilin bm) (bm i)) (bm j) = if i = j then Q (bm i) else if i < j then polar (⇑Q) (bm i) (bm j) else 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Field K
inst✝² : Module K V
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ ∀ (m : Matrix.SpecialLinearGroup ι K) (x : ℙ K (ι → K)),
    id (m • x) = (QuotientGroup.mk' (Subgroup.center (Matrix.SpecialLinearGroup ι K))) m • id x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Basis

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
⊢ (Q.toBilin bm).toQuadraticMap x = Q x

Tactic:
← bm.linearCombination_repr x,

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
⊢ (Q.toBilin bm).toQuadraticMap ((Finsupp.linearCombination R ⇑bm) (bm.repr x)) =
    Q ((Finsupp.linearCombination R ⇑bm) (bm.repr x))
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Field K
inst✝² : Module K V
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
u : Kˣ
v : ι → K
hv : v ≠ 0
⊢ u • v = (Matrix.GeneralLinearGroup.scalar ι) u • v

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Field K
inst✝² : Module K V
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
u : Kˣ
v : ι → K
hv : v ≠ 0
⊢ (Matrix.GeneralLinearGroup.scalar ι) u • mk K v hv = mk K v hv

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : Nontrivial R
hV : 1 ≤ Module.finrank R V
r : R := ⋯.choose
hr : r ^ max (Module.finrank R V) 1 = 1
⊢ IsUnit r

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : Nontrivial R
hV : 1 ≤ Module.finrank R V
r : R := ⋯.choose
hr : r ^ max (Module.finrank R V) 1 = 1
this : IsUnit r
⊢ this.unit ∈ rootsOfUnity (max (Module.finrank R V) 1) R

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : Nontrivial R
hV : Nontrivial V
⊢ ↥(rootsOfUnity (max (Module.finrank R V) 1) R)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g : ↥(Subgroup.center (SpecialLinearGroup R V))
⊢ centerEquivRootsOfUnity_invFun
      ((fun g ↦
          ⋯.by_cases (fun x ↦ 1) fun hR ↦
            ⋯.by_cases (fun x ↦ 1) fun hV ↦
              have hV := ⋯;
              have hr := ⋯;
              let r := ⋯.choose;
              have this := ⋯;
              ⟨this.unit, ⋯⟩)
        g) =
    g

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
hR : ¬Subsingleton R
hV✝ : ¬Subsingleton V
hV : Nontrivial V
this✝ : FaithfulSMul R V
H : ∃ r_1, r_1 ^ Module.finrank R V = 1 ∧ ↑↑↑(centerEquivRootsOfUnity_invFun r) = r_1 • LinearMap.id
this : H.choose • LinearMap.id = ↑↑r • LinearMap.id
⊢ ⋯.choose = ↑↑r

Tactic:
apply FaithfulSMul.eq_of_smul_eq_smul (α := V)

Goal state after:
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
hR : ¬Subsingleton R
hV✝ : ¬Subsingleton V
hV : Nontrivial V
this✝ : FaithfulSMul R V
H : ∃ r_1, r_1 ^ Module.finrank R V = 1 ∧ ↑↑↑(centerEquivRootsOfUnity_invFun r) = r_1 • LinearMap.id
this : H.choose • LinearMap.id = ↑↑r • LinearMap.id
⊢ ∀ (a : V), ⋯.choose • a = ↑↑r • a
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
hR : ¬Subsingleton R
hV✝ : ¬Subsingleton V
hV : Nontrivial V
this✝ : FaithfulSMul R V
H : ∃ r_1, r_1 ^ Module.finrank R V = 1 ∧ ↑↑↑(centerEquivRootsOfUnity_invFun r) = r_1 • LinearMap.id
this : H.choose • LinearMap.id = ↑↑r • LinearMap.id
⊢ ⋯.choose = ↑↑r

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Basis

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
⊢ (Q.toBilin bm).toQuadraticMap = Q

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Basis

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Free R M
⊢ Function.Surjective BilinMap.toQuadraticMap

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
⊢ (fun g ↦
        ⋯.by_cases (fun x ↦ 1) fun hR ↦
          ⋯.by_cases (fun x ↦ 1) fun hV ↦
            have hV := ⋯;
            have hr := ⋯;
            let r := ⋯.choose;
            have this := ⋯;
            ⟨this.unit, ⋯⟩)
      (centerEquivRootsOfUnity_invFun r) =
    r

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Basis

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
bm : Basis ι R M
Q₁ Q₂ : QuadraticMap R M N
⊢ (Q₁ + Q₂).toBilin bm = Q₁.toBilin bm + Q₂.toBilin bm

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Basis

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : LinearOrder ι
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
S : Type u_5
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
bm : Basis ι R M
s : S
Q : QuadraticMap R M N
⊢ (s • Q).toBilin bm = s • Q.toBilin bm

Tactic:
by

Goal state after: