mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : CharZero R
g h : SpecialLinearGroup n ℤ
⊢ (map (Int.castRingHom R)) g = (map (Int.castRingHom R)) h → g = h

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Fact (Even (Fintype.card n))
g : SpecialLinearGroup n R
⊢ (-↑g).det = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: R : Type v
inst✝ : CommRing R
A : SL(2, R)
⊢ det ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]] = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: R : Type v
inst✝ : CommRing R
A : SL(2, R)
⊢ A⁻¹ = ⟨![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]], ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
P : SL(2, R) → Prop
a b c d : R
hdet : a * d - b * c = 1
⊢ !![a, b; c, d].det = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: R : Type v
inst✝ : CommRing R
P : SL(2, R) → Prop
h : ∀ (a b c d : R) (hdet : a * d - b * c = 1), P ⟨!![a, b; c, d], ⋯⟩
m : Matrix (Fin 2) (Fin 2) R
hm : m.det = 1
⊢ m 0 0 * m 1 1 - m 0 1 * m 1 0 = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: R : Type v
inst✝ : CommRing R
P : SL(2, R) → Prop
h : ∀ (a b c d : R) (hdet : a * d - b * c = 1), P ⟨!![a, b; c, d], ⋯⟩
g : SL(2, R)
⊢ P g

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R✝ : Type v
inst✝² : CommRing R✝
S : Type u_1
inst✝¹ : CommRing S
R : Type u_2
inst✝ : Field R
g : SL(2, R)
hg : ↑g 1 0 = 0
a b : R
h : a ≠ 0
⊢ !![a, b; 0, a⁻¹].det = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: R : Type u_2
inst✝ : Field R
a b c d : R
h_det : a * d - b * c = 1
hg : ↑⟨!![a, b; c, d], ⋯⟩ 1 0 = 0
⊢ c = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: R : Type u_2
inst✝ : Field R
a b c d : R
h_det : a * d - b * c = 1
hg : c = 0
⊢ a * d = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: R : Type u_2
inst✝ : Field R
g : SL(2, R)
hg : ↑g 1 0 = 0
⊢ ∃ a b, ∃ (h : a ≠ 0), g = ⟨!![a, b; 0, a⁻¹], ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: R : Type v
inst✝ : CommRing R
A : SL(2, R)
i : Fin 2
⊢ IsCoprime (↑A i 0) (↑A i 1)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: R : Type v
inst✝ : CommRing R
A : SL(2, R)
j : Fin 2
⊢ IsCoprime (↑A 0 j) (↑A 1 j)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
hab : IsCoprime a b
j : Fin 2
⊢ ∃ g, ↑g 0 j = a ∧ ↑g 1 j = b

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
hab : IsCoprime a b
i : Fin 2
⊢ ∃ g, ↑g i 0 = a ∧ ↑g i 1 = b

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
v : Fin 2 → R
hab : IsCoprime (v 0) (v 1)
A g : SL(2, R)
hg : ↑g 0 0 = v 0 ∧ ↑g 0 1 = v 1
t : Fin 2
⊢ v t = ↑g 0 t

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
v : Fin 2 → R
hab : IsCoprime (v 0) (v 1)
A : SL(2, R)
⊢ IsCoprime ((v ᵥ* ↑A) 0) ((v ᵥ* ↑A) 1)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
g : CliffordAlgebra Q →ₐ[R] A
m : M
⊢ g ((ι Q) m) * g ((ι Q) m) = (algebraMap R A) (Q m)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
v : Fin 2 → R
hab : IsCoprime (v 0) (v 1)
A : SL(2, R)
⊢ IsCoprime ((↑A *ᵥ v) 0) ((↑A *ᵥ v) 1)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: ι : Type u_1
F : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommRing F
i j : ι
hij : i ≠ j
⊢ transvection hij 0 = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: ι : Type u_1
F : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommRing F
i j : ι
hij : i ≠ j
b : F
⊢ transvection hij b • Pi.single i 1 = Pi.single i 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: ι : Type u_1
F : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommRing F
i j : ι
hij : i ≠ j
b : F
⊢ ↑(transvection hij b) *ᵥ Pi.single i 1 = Pi.single i 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : { f // ∀ (m : M), f m * f m = (algebraMap R A) (Q m) }
x y : TensorAlgebra R M
h : Rel Q x y
⊢ (RingCon.ker ((TensorAlgebra.lift R) ↑f).toRingHom) x y

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: ι : Type u_1
F : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommRing F
i j : ι
hij : i ≠ j
b : F
⊢ transvection hij b • Pi.single j 1 = Pi.single j 1 + b • Pi.single i 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: ι : Type u_1
F : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommRing F
i j : ι
hij : i ≠ j
b : F
⊢ ↑(transvection hij b) *ᵥ Pi.single j 1 = Pi.single j 1 + b • Pi.single i 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: ι : Type u_1
F : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommRing F
i j : ι
hij : i ≠ j
b : F
⊢ ↑(transvection hij b * transvection hij (-b)) = ↑1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : { f // ∀ (m : M), f m * f m = (algebraMap R A) (Q m) }
⊢ ringCon Q ≤ RingCon.ker ((TensorAlgebra.lift R) ↑f).toRingHom

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: ι : Type u_1
F : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommRing F
i j : ι
hij : i ≠ j
b : F
⊢ transvection hij (-b) * transvection hij b = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: ι : Type u_1
F : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommRing F
i j : ι
hij : i ≠ j
b₁ b₂ : F
⊢ ↑(transvection hij (b₁ + b₂)) = ↑(transvection hij b₁ * transvection hij b₂)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: ι : Type u_1
F : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommRing F
i j : ι
hij : i ≠ j
b : F
⊢ transvection hij b ∈ Subgroup.center (SpecialLinearGroup ι F) ↔ b = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : CliffordAlgebra Q →ₐ[R] A
m : M
⊢ (F.toLinearMap ∘ₗ ι Q) m * (F.toLinearMap ∘ₗ ι Q) m = (algebraMap R A) (Q m)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
a : F
ha : a ≠ 0
⊢ {x | x = i} = {i}

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
a : F
ha : a ≠ 0
⊢ (diagonal fun k ↦ if k = i then a else if k = j then a⁻¹ else 1).det = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ ↑(diag2 a ha) =
    diagonal fun i ↦
      match i with
      | 0 => a
      | 1 => a⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : { f // ∀ (m : M), f m * f m = (algebraMap R A) (Q m) }
⊢ (fun F ↦ ⟨F.toLinearMap ∘ₗ ι Q, ⋯⟩) ((fun f ↦ (ringCon Q).liftₐ ((TensorAlgebra.lift R) ↑f) ⋯) f) = f

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ ↑(diag2 a ha) = !![a, 0; 0, a⁻¹]

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : CliffordAlgebra Q →ₐ[R] A
x : M
⊢ ((((fun f ↦ (ringCon Q).liftₐ ((TensorAlgebra.lift R) ↑f) ⋯) ((fun F ↦ ⟨F.toLinearMap ∘ₗ ι Q, ⋯⟩) F)).comp
            (RingCon.mkₐ R (ringCon Q))).toLinearMap ∘ₗ
        TensorAlgebra.ι R)
      x =
    ((F.comp (RingCon.mkₐ R (ringCon Q))).toLinearMap ∘ₗ TensorAlgebra.ι R) x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ diag2 a ha • Pi.single 0 1 = a • Pi.single 0 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ diag2 a ha • Pi.single 1 1 = a⁻¹ • Pi.single 1 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ ↑(diag2 a ha * diag2 a⁻¹ ⋯) = ↑1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ (diag2 a ha)⁻¹ = diag2 a⁻¹ ⋯

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : ∏ i ∈ insert i₀ {i | i ≠ i₀}, D i = 1
⊢ i₀ ∉ {i | i ≠ i₀}

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : D i₀ * ∏ x with x ≠ i₀, D x = 1
⊢ ∏ x with x ≠ i₀, D x ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
cond : ∀ (m : M), f m * f m = (algebraMap R A) (Q m)
g : CliffordAlgebra Q →ₐ[R] A
⊢ g.toLinearMap ∘ₗ ι Q = f ↔ g = (lift Q) ⟨f, cond⟩

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
g : CliffordAlgebra Q →ₐ[R] A
⊢ (lift Q) ⟨g.toLinearMap ∘ₗ ι Q, ⋯⟩ = g

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : D i₀ = ∏ x with x ≠ i₀, (D x)⁻¹
x : ι
hx : x = i₀
⊢ ∀ x ∈ {x | ¬x = i₀}, (if i₀ = x then D x else (D x)⁻¹) = (D x)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_4
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : CliffordAlgebra Q →ₐ[R] A
⊢ f.toLinearMap ∘ₗ ι Q = g.toLinearMap ∘ₗ ι Q → f = g

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : (diagonal D).det = 1
⊢ (∏ i with i ≠ i₀, fun k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1) = D

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → F
j : ι
hD : ∏ i ∈ insert j {i | i ≠ j}, D i = 1
h : D j = 0
⊢ j ∉ {i | i ≠ j}

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
C : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), C ((Algebra.algebraMap R (CliffordAlgebra Q)) r)
ι : ∀ (x : M), C ((CliffordAlgebra.ι Q) x)
mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)
add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)
a : CliffordAlgebra Q
s : Subalgebra R (CliffordAlgebra Q) :=
  { carrier := {a | C a}, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯,
    algebraMap_mem' := algebraMap }
of : { f // ∀ (m : M), f m * f m = (Algebra.algebraMap R ↥s) (Q m) } :=
  ⟨LinearMap.codRestrict (Subalgebra.toSubmodule s) (CliffordAlgebra.ι Q) ι, ⋯⟩
⊢ s.val.comp ((lift Q) of) = AlgHom.id R (CliffordAlgebra Q)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → F
hD : (diagonal D).det = 1
j : ι
h : D j = 0
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
C : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), C ((Algebra.algebraMap R (CliffordAlgebra Q)) r)
ι : ∀ (x : M), C ((CliffordAlgebra.ι Q) x)
mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)
add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)
a : CliffordAlgebra Q
⊢ C a

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ Algebra.adjoin R (Set.range ⇑(ι Q)) = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
cond : ∀ (m : M), f m * f m = (algebraMap R A) (Q m)
⊢ ((lift Q) ⟨f, cond⟩).range = Algebra.adjoin R (Set.range ⇑f)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_4
inst✝¹ : Ring A
inst✝ : Algebra R A
f : M →ₗ[R] A
hf : ∀ (x : M), f x * f x = (algebraMap R A) (Q x)
a b : M
⊢ f a * f b + f b * f a = f (a + b) * f (a + b) - f a * f a - f b * f b

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_4
inst✝¹ : Ring A
inst✝ : Algebra R A
f : M →ₗ[R] A
hf : ∀ (x : M), f x * f x = (algebraMap R A) (Q x)
a b : M
⊢ f (a + b) * f (a + b) - f a * f a - f b * f b =
    (algebraMap R A) (Q (a + b)) - (algebraMap R A) (Q a) - (algebraMap R A) (Q b)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : (diagonal D).det = 1
⊢ (↑{i | i ≠ i₀}).Pairwise (Function.onFun Commute fun i ↦ if hi : i ≠ i₀ then diag2n hi (D i) ⋯ else 1)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_4
inst✝¹ : Ring A
inst✝ : Algebra R A
f : M →ₗ[R] A
hf : ∀ (x : M), f x * f x = (algebraMap R A) (Q x)
a b : M
⊢ (algebraMap R A) (Q (a + b)) - (algebraMap R A) (Q a) - (algebraMap R A) (Q b) =
    (algebraMap R A) (Q (a + b) - Q a - Q b)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_4
inst✝¹ : Ring A
inst✝ : Algebra R A
h2 : IsUnit 2
f : M →ₗ[R] A
⊢ (∀ (x : M), f x * f x = (algebraMap R A) (Q x)) ↔
    (LinearMap.mul R A).compl₂ f ∘ₗ f + (LinearMap.mul R A).flip.compl₂ f ∘ₗ f =
      LinearMap.compr₂ (QuadraticMap.polarBilin Q) (Algebra.linearMap R A)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
a b : M
y : CliffordAlgebra Q
⊢ x * (ι Q) a * ((ι Q) b * y) =
    (algebraMap R (CliffordAlgebra Q)) (QuadraticMap.polar (⇑Q) a b) * (x * y) - x * (ι Q) b * ((ι Q) a * y)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a b : M
h : QuadraticMap.IsOrtho Q a b
⊢ (ι Q) a * (ι Q) b + (ι Q) b * (ι Q) a = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
a b : M
h : QuadraticMap.IsOrtho Q a b
⊢ x * (ι Q) a * (ι Q) b = -(x * (ι Q) b * (ι Q) a)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
a b : M
h : QuadraticMap.IsOrtho Q a b
⊢ (ι Q) a * ((ι Q) b * x) = -((ι Q) b * ((ι Q) a * x))

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : (diagonal D).det = 1
⊢ ⟨diagonal D, hD⟩ = {i | i ≠ i₀}.noncommProd (fun i ↦ if hi : i ≠ i₀ then diag2n hi (D i) ⋯ else 1) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
a b : M
h : QuadraticMap.IsOrtho Q a b
y : CliffordAlgebra Q
⊢ x * (ι Q) a * ((ι Q) b * y) = -(x * (ι Q) b * ((ι Q) a * y))

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : SpecialLinearGroup ι F
L L' : List (TransvectionStruct ι F)
D : ι → F
hM : ↑M = (List.map TransvectionStruct.toMatrix L).prod * diagonal D * (List.map TransvectionStruct.toMatrix L').prod
⊢ (diagonal D).det = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a b : M
⊢ (ι Q) a * (ι Q) b * (ι Q) a = (ι Q) (QuadraticMap.polar (⇑Q) a b • a - Q a • b)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
cond : ∀ (m : M), f m * f m = (algebraMap R A) (Q m)
⊢ Submodule.map ((lift Q) ⟨f, cond⟩).toLinearMap (ι Q).range = f.range

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M₁ : Type u_4
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
Q₁ : QuadraticForm R M₁
⊢ map (QuadraticMap.Isometry.id Q₁) = AlgHom.id R (CliffordAlgebra Q₁)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : Q₂ →qᵢ Q₃
g : Q₁ →qᵢ Q₂
⊢ (map f).comp (map g) = map (f.comp g)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
f : Q₁ →qᵢ Q₂
g : Q₂ →qᵢ Q₁
h : LeftInverse ⇑g ⇑f
⊢ LeftInverse ⇑(map g) ⇑(map f)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
f : Q₁ →qᵢ Q₂
hf : Function.Surjective ⇑f
r : R
⊢ (map f) ((algebraMap R (CliffordAlgebra Q₁)) r) = (algebraMap R (CliffordAlgebra Q₂)) r

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
f : Q₁ →qᵢ Q₂
hf : Function.Surjective ⇑f
y : M₂
x : M₁
hx : f x = y
⊢ (map f) ((ι Q₁) x) = (ι Q₂) y

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : SpecialLinearGroup ι F
⊢ ∃ L L' D,
    ∃ (hD : (diagonal D).det = 1),
      M =
        (List.map TransvectionStruct.toSpecialLinearGroup L).prod * ⟨diagonal D, hD⟩ *
          (List.map TransvectionStruct.toSpecialLinearGroup L').prod

Tactic:
by

Goal state after: