Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - fix: denote alternating map by ⋀, not Λ #11064

Closed
wants to merge 4 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions Mathlib/Analysis/InnerProductSpace/Orientation.lean
Original file line number Diff line number Diff line change
Expand Up @@ -93,7 +93,7 @@ theorem det_eq_neg_det_of_opposite_orientation (h : e.toBasis.orientation ≠ f.
rw [e.toBasis.det.eq_smul_basis_det f.toBasis]
-- Porting note: added `neg_one_smul` with explicit type
simp [e.det_to_matrix_orthonormalBasis_of_opposite_orientation f h,
neg_one_smul ℝ (M := E [Λ^ι]→ₗ[ℝ] ℝ)]
neg_one_smul ℝ (M := E [^ι]→ₗ[ℝ] ℝ)]
#align orthonormal_basis.det_eq_neg_det_of_opposite_orientation OrthonormalBasis.det_eq_neg_det_of_opposite_orientation

section AdjustToOrientation
Expand Down Expand Up @@ -178,10 +178,10 @@ variable [_i : Fact (finrank ℝ E = n)] (o : Orientation ℝ E (Fin n))
/-- The volume form on an oriented real inner product space, a nonvanishing top-dimensional
alternating form uniquely defined by compatibility with the orientation and inner product structure.
-/
irreducible_def volumeForm : E [Λ^Fin n]→ₗ[ℝ] ℝ := by
irreducible_def volumeForm : E [^Fin n]→ₗ[ℝ] ℝ := by
classical
cases' n with n
· let opos : E [Λ^Fin 0]→ₗ[ℝ] ℝ := .constOfIsEmpty ℝ E (Fin 0) (1 : ℝ)
· let opos : E [^Fin 0]→ₗ[ℝ] ℝ := .constOfIsEmpty ℝ E (Fin 0) (1 : ℝ)
exact o.eq_or_eq_neg_of_isEmpty.by_cases (fun _ => opos) fun _ => -opos
· exact (o.finOrthonormalBasis n.succ_pos _i.out).toBasis.det
#align orientation.volume_form Orientation.volumeForm
Expand Down
6 changes: 3 additions & 3 deletions Mathlib/Analysis/InnerProductSpace/TwoDim.lean
Original file line number Diff line number Diff line change
Expand Up @@ -93,10 +93,10 @@ namespace Orientation
notation `ω`). When evaluated on two vectors, it gives the oriented area of the parallelogram they
span. -/
irreducible_def areaForm : E →ₗ[ℝ] E →ₗ[ℝ] ℝ := by
let z : E [Λ^Fin 0]→ₗ[ℝ] ℝ ≃ₗ[ℝ] ℝ :=
let z : E [^Fin 0]→ₗ[ℝ] ℝ ≃ₗ[ℝ] ℝ :=
AlternatingMap.constLinearEquivOfIsEmpty.symm
let y : E [Λ^Fin 1]→ₗ[ℝ] ℝ →ₗ[ℝ] E →ₗ[ℝ] ℝ :=
LinearMap.llcomp ℝ E (E [Λ^Fin 0]→ₗ[ℝ] ℝ) ℝ z ∘ₗ AlternatingMap.curryLeftLinearMap
let y : E [^Fin 1]→ₗ[ℝ] ℝ →ₗ[ℝ] E →ₗ[ℝ] ℝ :=
LinearMap.llcomp ℝ E (E [^Fin 0]→ₗ[ℝ] ℝ) ℝ z ∘ₗ AlternatingMap.curryLeftLinearMap
exact y ∘ₗ AlternatingMap.curryLeftLinearMap (R' := ℝ) o.volumeForm
#align orientation.area_form Orientation.areaForm

Expand Down
194 changes: 97 additions & 97 deletions Mathlib/LinearAlgebra/Alternating/Basic.lean

Large diffs are not rendered by default.

26 changes: 13 additions & 13 deletions Mathlib/LinearAlgebra/Alternating/DomCoprod.lean
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,7 @@ open Equiv
variable [DecidableEq ιa] [DecidableEq ιb]

/-- summand used in `AlternatingMap.domCoprod` -/
def domCoprod.summand (a : Mᵢ [Λ^ιa]→ₗ[R'] N₁) (b : Mᵢ [Λ^ιb]→ₗ[R'] N₂)
def domCoprod.summand (a : Mᵢ [^ιa]→ₗ[R'] N₁) (b : Mᵢ [^ιb]→ₗ[R'] N₂)
(σ : Perm.ModSumCongr ιa ιb) : MultilinearMap R' (fun _ : Sum ιa ιb => Mᵢ) (N₁ ⊗[R'] N₂) :=
Quotient.liftOn' σ
(fun σ =>
Expand All @@ -66,7 +66,7 @@ def domCoprod.summand (a : Mᵢ [Λ^ιa]→ₗ[R'] N₁) (b : Mᵢ [Λ^ιb]→
erw [← a.map_congr_perm fun i => v (σ₁ _), ← b.map_congr_perm fun i => v (σ₁ _)]
#align alternating_map.dom_coprod.summand AlternatingMap.domCoprod.summand

theorem domCoprod.summand_mk'' (a : Mᵢ [Λ^ιa]→ₗ[R'] N₁) (b : Mᵢ [Λ^ιb]→ₗ[R'] N₂)
theorem domCoprod.summand_mk'' (a : Mᵢ [^ιa]→ₗ[R'] N₁) (b : Mᵢ [^ιb]→ₗ[R'] N₂)
(σ : Equiv.Perm (Sum ιa ιb)) :
domCoprod.summand a b (Quotient.mk'' σ) =
Equiv.Perm.sign σ •
Expand All @@ -76,8 +76,8 @@ theorem domCoprod.summand_mk'' (a : Mᵢ [Λ^ιa]→ₗ[R'] N₁) (b : Mᵢ [Λ^
#align alternating_map.dom_coprod.summand_mk' AlternatingMap.domCoprod.summand_mk''

/-- Swapping elements in `σ` with equal values in `v` results in an addition that cancels -/
theorem domCoprod.summand_add_swap_smul_eq_zero (a : Mᵢ [Λ^ιa]→ₗ[R'] N₁)
(b : Mᵢ [Λ^ιb]→ₗ[R'] N₂) (σ : Perm.ModSumCongr ιa ιb) {v : Sum ιa ιb → Mᵢ}
theorem domCoprod.summand_add_swap_smul_eq_zero (a : Mᵢ [^ιa]→ₗ[R'] N₁)
(b : Mᵢ [^ιb]→ₗ[R'] N₂) (σ : Perm.ModSumCongr ιa ιb) {v : Sum ιa ιb → Mᵢ}
{i j : Sum ιa ιb} (hv : v i = v j) (hij : i ≠ j) :
domCoprod.summand a b σ v + domCoprod.summand a b (swap i j • σ) v = 0 := by
refine Quotient.inductionOn' σ fun σ => ?_
Expand All @@ -94,8 +94,8 @@ theorem domCoprod.summand_add_swap_smul_eq_zero (a : Mᵢ [Λ^ιa]→ₗ[R'] N

/-- Swapping elements in `σ` with equal values in `v` result in zero if the swap has no effect
on the quotient. -/
theorem domCoprod.summand_eq_zero_of_smul_invariant (a : Mᵢ [Λ^ιa]→ₗ[R'] N₁)
(b : Mᵢ [Λ^ιb]→ₗ[R'] N₂) (σ : Perm.ModSumCongr ιa ιb) {v : Sum ιa ιb → Mᵢ}
theorem domCoprod.summand_eq_zero_of_smul_invariant (a : Mᵢ [^ιa]→ₗ[R'] N₁)
(b : Mᵢ [^ιb]→ₗ[R'] N₂) (σ : Perm.ModSumCongr ιa ιb) {v : Sum ιa ιb → Mᵢ}
{i j : Sum ιa ιb} (hv : v i = v j) (hij : i ≠ j) :
swap i j • σ = σ → domCoprod.summand a b σ v = 0 := by
refine Quotient.inductionOn' σ fun σ => ?_
Expand Down Expand Up @@ -154,8 +154,8 @@ The specialized version can be obtained by combining this definition with `finSu
`LinearMap.mul'`.
-/
@[simps]
def domCoprod (a : Mᵢ [Λ^ιa]→ₗ[R'] N₁) (b : Mᵢ [Λ^ιb]→ₗ[R'] N₂) :
Mᵢ [Λ^ιa ⊕ ιb]→ₗ[R'] (N₁ ⊗[R'] N₂) :=
def domCoprod (a : Mᵢ [^ιa]→ₗ[R'] N₁) (b : Mᵢ [^ιb]→ₗ[R'] N₂) :
Mᵢ [^ιa ⊕ ιb]→ₗ[R'] (N₁ ⊗[R'] N₂) :=
{ ∑ σ : Perm.ModSumCongr ιa ιb, domCoprod.summand a b σ with
toFun := fun v => (⇑(∑ σ : Perm.ModSumCongr ιa ιb, domCoprod.summand a b σ)) v
map_eq_zero_of_eq' := fun v i j hv hij => by
Expand All @@ -170,7 +170,7 @@ def domCoprod (a : Mᵢ [Λ^ιa]→ₗ[R'] N₁) (b : Mᵢ [Λ^ιb]→ₗ[R'] N
#align alternating_map.dom_coprod AlternatingMap.domCoprod
#align alternating_map.dom_coprod_apply AlternatingMap.domCoprod_apply

theorem domCoprod_coe (a : Mᵢ [Λ^ιa]→ₗ[R'] N₁) (b : Mᵢ [Λ^ιb]→ₗ[R'] N₂) :
theorem domCoprod_coe (a : Mᵢ [^ιa]→ₗ[R'] N₁) (b : Mᵢ [^ιb]→ₗ[R'] N₂) :
(↑(a.domCoprod b) : MultilinearMap R' (fun _ => Mᵢ) _) =
∑ σ : Perm.ModSumCongr ιa ιb, domCoprod.summand a b σ :=
MultilinearMap.ext fun _ => rfl
Expand All @@ -179,8 +179,8 @@ theorem domCoprod_coe (a : Mᵢ [Λ^ιa]→ₗ[R'] N₁) (b : Mᵢ [Λ^ιb]→
/-- A more bundled version of `AlternatingMap.domCoprod` that maps
`((ι₁ → N) → N₁) ⊗ ((ι₂ → N) → N₂)` to `(ι₁ ⊕ ι₂ → N) → N₁ ⊗ N₂`. -/
def domCoprod' :
(Mᵢ [Λ^ιa]→ₗ[R'] N₁) ⊗[R'] (Mᵢ [Λ^ιb]→ₗ[R'] N₂) →ₗ[R']
(Mᵢ [Λ^ιa ⊕ ιb]→ₗ[R'] (N₁ ⊗[R'] N₂)) :=
(Mᵢ [^ιa]→ₗ[R'] N₁) ⊗[R'] (Mᵢ [^ιb]→ₗ[R'] N₂) →ₗ[R']
(Mᵢ [^ιa ⊕ ιb]→ₗ[R'] (N₁ ⊗[R'] N₂)) :=
TensorProduct.lift <| by
refine'
LinearMap.mk₂ R' domCoprod (fun m₁ m₂ n => _) (fun c m n => _) (fun m n₁ n₂ => _)
Expand All @@ -200,7 +200,7 @@ def domCoprod' :
#align alternating_map.dom_coprod' AlternatingMap.domCoprod'

@[simp]
theorem domCoprod'_apply (a : Mᵢ [Λ^ιa]→ₗ[R'] N₁) (b : Mᵢ [Λ^ιb]→ₗ[R'] N₂) :
theorem domCoprod'_apply (a : Mᵢ [^ιa]→ₗ[R'] N₁) (b : Mᵢ [^ιb]→ₗ[R'] N₂) :
domCoprod' (a ⊗ₜ[R'] b) = domCoprod a b :=
rfl
#align alternating_map.dom_coprod'_apply AlternatingMap.domCoprod'_apply
Expand Down Expand Up @@ -271,7 +271,7 @@ theorem MultilinearMap.domCoprod_alternization [DecidableEq ιa] [DecidableEq ι
`AlternatingMap`s gives a scaled version of the `AlternatingMap.coprod` of those maps.
-/
theorem MultilinearMap.domCoprod_alternization_eq [DecidableEq ιa] [DecidableEq ιb]
(a : Mᵢ [Λ^ιa]→ₗ[R'] N₁) (b : Mᵢ [Λ^ιb]→ₗ[R'] N₂) :
(a : Mᵢ [^ιa]→ₗ[R'] N₁) (b : Mᵢ [^ιb]→ₗ[R'] N₂) :
MultilinearMap.alternatization
(MultilinearMap.domCoprod a b : MultilinearMap R' (fun _ : Sum ιa ιb => Mᵢ) (N₁ ⊗ N₂)) =
((Fintype.card ιa).factorial * (Fintype.card ιb).factorial) • a.domCoprod b := by
Expand Down
8 changes: 4 additions & 4 deletions Mathlib/LinearAlgebra/Determinant.lean
Original file line number Diff line number Diff line change
Expand Up @@ -504,7 +504,7 @@ theorem LinearMap.associated_det_comp_equiv {N : Type*} [AddCommGroup N] [Module

/-- The determinant of a family of vectors with respect to some basis, as an alternating
multilinear map. -/
nonrec def Basis.det : M [Λ^ι]→ₗ[R] R where
nonrec def Basis.det : M [^ι]→ₗ[R] R where
toFun v := det (e.toMatrix v)
map_add' := by
intro inst v i x y
Expand Down Expand Up @@ -570,7 +570,7 @@ theorem Basis.isUnit_det (e' : Basis ι R M) : IsUnit (e.det e') :=

/-- Any alternating map to `R` where `ι` has the cardinality of a basis equals the determinant
map with respect to that basis, multiplied by the value of that alternating map on that basis. -/
theorem AlternatingMap.eq_smul_basis_det (f : M [Λ^ι]→ₗ[R] R) : f = f e • e.det := by
theorem AlternatingMap.eq_smul_basis_det (f : M [^ι]→ₗ[R] R) : f = f e • e.det := by
refine' Basis.ext_alternating e fun i h => _
let σ : Equiv.Perm ι := Equiv.ofBijective i (Finite.injective_iff_bijective.1 h)
change f (e ∘ σ) = (f e • e.det) (e ∘ σ)
Expand All @@ -579,7 +579,7 @@ theorem AlternatingMap.eq_smul_basis_det (f : M [Λ^ι]→ₗ[R] R) : f = f e

@[simp]
theorem AlternatingMap.map_basis_eq_zero_iff {ι : Type*} [Finite ι] (e : Basis ι R M)
(f : M [Λ^ι]→ₗ[R] R) : f e = 0 ↔ f = 0 :=
(f : M [^ι]→ₗ[R] R) : f e = 0 ↔ f = 0 :=
⟨fun h => by
cases nonempty_fintype ι
letI := Classical.decEq ι
Expand All @@ -588,7 +588,7 @@ theorem AlternatingMap.map_basis_eq_zero_iff {ι : Type*} [Finite ι] (e : Basis
#align alternating_map.map_basis_eq_zero_iff AlternatingMap.map_basis_eq_zero_iff

theorem AlternatingMap.map_basis_ne_zero_iff {ι : Type*} [Finite ι] (e : Basis ι R M)
(f : M [Λ^ι]→ₗ[R] R) : f e ≠ 0 ↔ f ≠ 0 :=
(f : M [^ι]→ₗ[R] R) : f e ≠ 0 ↔ f ≠ 0 :=
not_congr <| f.map_basis_eq_zero_iff e
#align alternating_map.map_basis_ne_zero_iff AlternatingMap.map_basis_ne_zero_iff

Expand Down
2 changes: 1 addition & 1 deletion Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -275,7 +275,7 @@ variable (R)

This is a special case of `MultilinearMap.mkPiAlgebraFin`, and the exterior algebra version of
`TensorAlgebra.tprod`. -/
def ιMulti (n : ℕ) : M [Λ^Fin n]→ₗ[R] ExteriorAlgebra R M :=
def ιMulti (n : ℕ) : M [^Fin n]→ₗ[R] ExteriorAlgebra R M :=
let F := (MultilinearMap.mkPiAlgebraFin R n (ExteriorAlgebra R M)).compLinearMap fun _ => ι R
{ F with
map_eq_zero_of_eq' := fun f x y hfxy hxy => by
Expand Down
24 changes: 12 additions & 12 deletions Mathlib/LinearAlgebra/ExteriorAlgebra/OfAlternating.lean
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ variable [Module R M] [Module R N] [Module R N']

-- This instance can't be found where it's needed if we don't remind lean that it exists.
instance AlternatingMap.instModuleAddCommGroup {ι : Type*} :
Module R (M [Λ^ι]→ₗ[R] N) := by
Module R (M [^ι]→ₗ[R] N) := by
infer_instance
#align alternating_map.module_add_comm_group AlternatingMap.instModuleAddCommGroup

Expand All @@ -43,10 +43,10 @@ open CliffordAlgebra hiding ι

/-- Build a map out of the exterior algebra given a collection of alternating maps acting on each
exterior power -/
def liftAlternating : (∀ i, M [Λ^Fin i]→ₗ[R] N) →ₗ[R] ExteriorAlgebra R M →ₗ[R] N := by
def liftAlternating : (∀ i, M [^Fin i]→ₗ[R] N) →ₗ[R] ExteriorAlgebra R M →ₗ[R] N := by
suffices
(∀ i, M [Λ^Fin i]→ₗ[R] N) →ₗ[R]
ExteriorAlgebra R M →ₗ[R] ∀ i, M [Λ^Fin i]→ₗ[R] N by
(∀ i, M [^Fin i]→ₗ[R] N) →ₗ[R]
ExteriorAlgebra R M →ₗ[R] ∀ i, M [^Fin i]→ₗ[R] N by
refine' LinearMap.compr₂ this _
refine' (LinearEquiv.toLinearMap _).comp (LinearMap.proj 0)
exact AlternatingMap.constLinearEquivOfIsEmpty.symm
Expand All @@ -67,7 +67,7 @@ def liftAlternating : (∀ i, M [Λ^Fin i]→ₗ[R] N) →ₗ[R] ExteriorAlgebra
#align exterior_algebra.lift_alternating ExteriorAlgebra.liftAlternating

@[simp]
theorem liftAlternating_ι (f : ∀ i, M [Λ^Fin i]→ₗ[R] N) (m : M) :
theorem liftAlternating_ι (f : ∀ i, M [^Fin i]→ₗ[R] N) (m : M) :
liftAlternating (R := R) (M := M) (N := N) f (ι R m) = f 1 ![m] := by
dsimp [liftAlternating]
rw [foldl_ι, LinearMap.mk₂_apply, AlternatingMap.curryLeft_apply_apply]
Expand All @@ -78,7 +78,7 @@ theorem liftAlternating_ι (f : ∀ i, M [Λ^Fin i]→ₗ[R] N) (m : M) :
rw [Matrix.zero_empty]
#align exterior_algebra.lift_alternating_ι ExteriorAlgebra.liftAlternating_ι

theorem liftAlternating_ι_mul (f : ∀ i, M [Λ^Fin i]→ₗ[R] N) (m : M)
theorem liftAlternating_ι_mul (f : ∀ i, M [^Fin i]→ₗ[R] N) (m : M)
(x : ExteriorAlgebra R M) :
liftAlternating (R := R) (M := M) (N := N) f (ι R m * x) =
liftAlternating (R := R) (M := M) (N := N) (fun i => (f i.succ).curryLeft m) x := by
Expand All @@ -88,21 +88,21 @@ theorem liftAlternating_ι_mul (f : ∀ i, M [Λ^Fin i]→ₗ[R] N) (m : M)
#align exterior_algebra.lift_alternating_ι_mul ExteriorAlgebra.liftAlternating_ι_mul

@[simp]
theorem liftAlternating_one (f : ∀ i, M [Λ^Fin i]→ₗ[R] N) :
theorem liftAlternating_one (f : ∀ i, M [^Fin i]→ₗ[R] N) :
liftAlternating (R := R) (M := M) (N := N) f (1 : ExteriorAlgebra R M) = f 0 0 := by
dsimp [liftAlternating]
rw [foldl_one]
#align exterior_algebra.lift_alternating_one ExteriorAlgebra.liftAlternating_one

@[simp]
theorem liftAlternating_algebraMap (f : ∀ i, M [Λ^Fin i]→ₗ[R] N) (r : R) :
theorem liftAlternating_algebraMap (f : ∀ i, M [^Fin i]→ₗ[R] N) (r : R) :
liftAlternating (R := R) (M := M) (N := N) f (algebraMap _ (ExteriorAlgebra R M) r) =
r • f 0 0 := by
rw [Algebra.algebraMap_eq_smul_one, map_smul, liftAlternating_one]
#align exterior_algebra.lift_alternating_algebra_map ExteriorAlgebra.liftAlternating_algebraMap

@[simp]
theorem liftAlternating_apply_ιMulti {n : ℕ} (f : ∀ i, M [Λ^Fin i]→ₗ[R] N)
theorem liftAlternating_apply_ιMulti {n : ℕ} (f : ∀ i, M [^Fin i]→ₗ[R] N)
(v : Fin n → M) : liftAlternating (R := R) (M := M) (N := N) f (ιMulti R n v) = f n v := by
rw [ιMulti_apply]
-- porting note: `v` is generalized automatically so it was removed from the next line
Expand All @@ -118,13 +118,13 @@ theorem liftAlternating_apply_ιMulti {n : ℕ} (f : ∀ i, M [Λ^Fin i]→ₗ[R
#align exterior_algebra.lift_alternating_apply_ι_multi ExteriorAlgebra.liftAlternating_apply_ιMulti

@[simp]
theorem liftAlternating_comp_ιMulti {n : ℕ} (f : ∀ i, M [Λ^Fin i]→ₗ[R] N) :
theorem liftAlternating_comp_ιMulti {n : ℕ} (f : ∀ i, M [^Fin i]→ₗ[R] N) :
(liftAlternating (R := R) (M := M) (N := N) f).compAlternatingMap (ιMulti R n) = f n :=
AlternatingMap.ext <| liftAlternating_apply_ιMulti f
#align exterior_algebra.lift_alternating_comp_ι_multi ExteriorAlgebra.liftAlternating_comp_ιMulti

@[simp]
theorem liftAlternating_comp (g : N →ₗ[R] N') (f : ∀ i, M [Λ^Fin i]→ₗ[R] N) :
theorem liftAlternating_comp (g : N →ₗ[R] N') (f : ∀ i, M [^Fin i]→ₗ[R] N) :
(liftAlternating (R := R) (M := M) (N := N') fun i => g.compAlternatingMap (f i)) =
g ∘ₗ liftAlternating (R := R) (M := M) (N := N) f := by
ext v
Expand Down Expand Up @@ -152,7 +152,7 @@ theorem liftAlternating_ιMulti :

/-- `ExteriorAlgebra.liftAlternating` is an equivalence. -/
@[simps apply symm_apply]
def liftAlternatingEquiv : (∀ i, M [Λ^Fin i]→ₗ[R] N) ≃ₗ[R] ExteriorAlgebra R M →ₗ[R] N
def liftAlternatingEquiv : (∀ i, M [^Fin i]→ₗ[R] N) ≃ₗ[R] ExteriorAlgebra R M →ₗ[R] N
where
toFun := liftAlternating (R := R)
map_add' := map_add _
Expand Down
14 changes: 7 additions & 7 deletions Mathlib/LinearAlgebra/Matrix/Determinant.lean
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,7 @@ variable {R : Type v} [CommRing R]
local notation "ε " σ:arg => ((sign σ : ℤ) : R)

/-- `det` is an `AlternatingMap` in the rows of the matrix. -/
def detRowAlternating : (n → R) [Λ^n]→ₗ[R] R :=
def detRowAlternating : (n → R) [^n]→ₗ[R] R :=
MultilinearMap.alternatization ((MultilinearMap.mkPiAlgebra R n R).compLinearMap LinearMap.proj)
#align matrix.det_row_alternating Matrix.detRowAlternating

Expand Down Expand Up @@ -91,7 +91,7 @@ theorem det_diagonal {d : n → R} : det (diagonal d) = ∏ i, d i := by

-- @[simp] -- Porting note (#10618): simp can prove this
theorem det_zero (_ : Nonempty n) : det (0 : Matrix n n R) = 0 :=
(detRowAlternating : (n → R) [Λ^n]→ₗ[R] R).map_zero
(detRowAlternating : (n → R) [^n]→ₗ[R] R).map_zero
#align matrix.det_zero Matrix.det_zero

@[simp]
Expand Down Expand Up @@ -240,7 +240,7 @@ theorem det_transpose (M : Matrix n n R) : Mᵀ.det = M.det := by
/-- Permuting the columns changes the sign of the determinant. -/
theorem det_permute (σ : Perm n) (M : Matrix n n R) :
(Matrix.det fun i => M (σ i)) = Perm.sign σ * M.det :=
((detRowAlternating : (n → R) [Λ^n]→ₗ[R] R).map_perm M σ).trans (by simp [Units.smul_def])
((detRowAlternating : (n → R) [^n]→ₗ[R] R).map_perm M σ).trans (by simp [Units.smul_def])
#align matrix.det_permute Matrix.det_permute

/-- Permuting rows and columns with the same equivalence has no effect. -/
Expand Down Expand Up @@ -362,7 +362,7 @@ Prove that a matrix with a repeated column has determinant equal to zero.


theorem det_eq_zero_of_row_eq_zero {A : Matrix n n R} (i : n) (h : ∀ j, A i j = 0) : det A = 0 :=
(detRowAlternating : (n → R) [Λ^n]→ₗ[R] R).map_coord_zero i (funext h)
(detRowAlternating : (n → R) [^n]→ₗ[R] R).map_coord_zero i (funext h)
#align matrix.det_eq_zero_of_row_eq_zero Matrix.det_eq_zero_of_row_eq_zero

theorem det_eq_zero_of_column_eq_zero {A : Matrix n n R} (j : n) (h : ∀ i, A i j = 0) :
Expand All @@ -375,7 +375,7 @@ variable {M : Matrix n n R} {i j : n}

/-- If a matrix has a repeated row, the determinant will be zero. -/
theorem det_zero_of_row_eq (i_ne_j : i ≠ j) (hij : M i = M j) : M.det = 0 :=
(detRowAlternating : (n → R) [Λ^n]→ₗ[R] R).map_eq_zero_of_eq M hij i_ne_j
(detRowAlternating : (n → R) [^n]→ₗ[R] R).map_eq_zero_of_eq M hij i_ne_j
#align matrix.det_zero_of_row_eq Matrix.det_zero_of_row_eq

/-- If a matrix has a repeated column, the determinant will be zero. -/
Expand All @@ -388,7 +388,7 @@ end DetZero

theorem det_updateRow_add (M : Matrix n n R) (j : n) (u v : n → R) :
det (updateRow M j <| u + v) = det (updateRow M j u) + det (updateRow M j v) :=
(detRowAlternating : (n → R) [Λ^n]→ₗ[R] R).map_add M j u v
(detRowAlternating : (n → R) [^n]→ₗ[R] R).map_add M j u v
#align matrix.det_update_row_add Matrix.det_updateRow_add

theorem det_updateColumn_add (M : Matrix n n R) (j : n) (u v : n → R) :
Expand All @@ -399,7 +399,7 @@ theorem det_updateColumn_add (M : Matrix n n R) (j : n) (u v : n → R) :

theorem det_updateRow_smul (M : Matrix n n R) (j : n) (s : R) (u : n → R) :
det (updateRow M j <| s • u) = s * det (updateRow M j u) :=
(detRowAlternating : (n → R) [Λ^n]→ₗ[R] R).map_smul M j s u
(detRowAlternating : (n → R) [^n]→ₗ[R] R).map_smul M j s u
#align matrix.det_update_row_smul Matrix.det_updateRow_smul

theorem det_updateColumn_smul (M : Matrix n n R) (j : n) (s : R) (u : n → R) :
Expand Down
Loading
Loading