R : Type u_1
inst✝⁵ : LinearOrderedCommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial R
e : Basis ι R M
i : ι
⊢ (-1 * ∏ x in Finset.univ \ {i}, OfNat.ofNat 1 x)⁻¹ • Basis.orientation e = -Basis.orientation e
R : Type u_1
inst✝⁵ : LinearOrderedCommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial R
e : Basis ι R M
i : ι
⊢ Basis.orientation (unitsSMul e (Function.update 1 i (-1))) = -Basis.orientation e
rw [orientation_unitsSMul, Finset.prod_update_of_mem (Finset.mem_univ _)]
no goals
R : Type u_1
inst✝⁵ : LinearOrderedCommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial R
e : Basis ι R M
i : ι
⊢ (-1 * ∏ x in Finset.univ \ {i}, OfNat.ofNat 1 x)⁻¹ • Basis.orientation e = -Basis.orientation e
simp