case intro
R : Type u_2
inst✝⁵ : StrictOrderedCommRing R
M : Type u_3
N : Type ?u.45806
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
ι : Type u_1
inst✝ : Finite ι
e : Basis ι R M
x : Orientation R M ι
f : M ≃ₗ[R] M
val✝ : Fintype ι
⊢ ↑(Orientation.map ι f) x = (↑LinearEquiv.det f)⁻¹ • x
R : Type u_2
inst✝⁵ : StrictOrderedCommRing R
M : Type u_3
N : Type ?u.45806
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
ι : Type u_1
inst✝ : Finite ι
e : Basis ι R M
x : Orientation R M ι
f : M ≃ₗ[R] M
⊢ ↑(Orientation.map ι f) x = (↑LinearEquiv.det f)⁻¹ • x
cases nonempty_fintype ι
case intro
R : Type u_2
inst✝⁵ : StrictOrderedCommRing R
M : Type u_3
N : Type ?u.45806
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
ι : Type u_1
inst✝ : Finite ι
e : Basis ι R M
x : Orientation R M ι
f : M ≃ₗ[R] M
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
⊢ ↑(Orientation.map ι f) x = (↑LinearEquiv.det f)⁻¹ • x
case intro
R : Type u_2
inst✝⁵ : StrictOrderedCommRing R
M : Type u_3
N : Type ?u.45806
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
ι : Type u_1
inst✝ : Finite ι
e : Basis ι R M
x : Orientation R M ι
f : M ≃ₗ[R] M
val✝ : Fintype ι
⊢ ↑(Orientation.map ι f) x = (↑LinearEquiv.det f)⁻¹ • x
letI := Classical.decEq ι
case intro.h
R : Type u_2
inst✝⁵ : StrictOrderedCommRing R
M : Type u_3
N : Type ?u.45806
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
ι : Type u_1
inst✝ : Finite ι
e : Basis ι R M
f : M ≃ₗ[R] M
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
g : AlternatingMap R M R ι
hg : g ≠ 0
⊢ ↑(Orientation.map ι f) (rayOfNeZero R g hg) = (↑LinearEquiv.det f)⁻¹ • rayOfNeZero R g hg
case intro
R : Type u_2
inst✝⁵ : StrictOrderedCommRing R
M : Type u_3
N : Type ?u.45806
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
ι : Type u_1
inst✝ : Finite ι
e : Basis ι R M
x : Orientation R M ι
f : M ≃ₗ[R] M
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
⊢ ↑(Orientation.map ι f) x = (↑LinearEquiv.det f)⁻¹ • x
induction' x using Module.Ray.ind with g hg
no goals
case intro.h
R : Type u_2
inst✝⁵ : StrictOrderedCommRing R
M : Type u_3
N : Type ?u.45806
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
ι : Type u_1
inst✝ : Finite ι
e : Basis ι R M
f : M ≃ₗ[R] M
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
g : AlternatingMap R M R ι
hg : g ≠ 0
⊢ ↑(Orientation.map ι f) (rayOfNeZero R g hg) = (↑LinearEquiv.det f)⁻¹ • rayOfNeZero R g hg
rw [Orientation.map_apply, smul_rayOfNeZero, ray_eq_iff, Units.smul_def,
  (g.compLinearMap f.symm).eq_smul_basis_det e, g.eq_smul_basis_det e,
  AlternatingMap.compLinearMap_apply, AlternatingMap.smul_apply,
  show (fun i ↦ (LinearEquiv.symm f).toLinearMap (e i)) = (LinearEquiv.symm f).toLinearMap ∘ e
  by rfl, Basis.det_comp, Basis.det_self, mul_one, smul_eq_mul, mul_comm, mul_smul,
  LinearEquiv.coe_inv_det]
no goals
R : Type u_2
inst✝⁵ : StrictOrderedCommRing R
M : Type u_3
N : Type ?u.45806
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
ι : Type u_1
inst✝ : Finite ι
e : Basis ι R M
f : M ≃ₗ[R] M
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
g : AlternatingMap R M R ι
hg : g ≠ 0
⊢ (fun i => ↑↑(LinearEquiv.symm f) (↑e i)) = ↑↑(LinearEquiv.symm f) ∘ ↑e
rfl