case h
R : Type u_2
inst✝⁴ : LinearOrderedCommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
x : AlternatingMap R M R ι
hx : x ≠ 0
⊢ rayOfNeZero R x hx = Basis.orientation e ∨ rayOfNeZero R x hx = -Basis.orientation e
R : Type u_2
inst✝⁴ : LinearOrderedCommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
x : Orientation R M ι
⊢ x = Basis.orientation e ∨ x = -Basis.orientation e
induction' x using Module.Ray.ind with x hx
case h
R : Type u_2
inst✝⁴ : LinearOrderedCommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
x : AlternatingMap R M R ι
hx✝ : x ≠ 0
hx : ↑x ↑e ≠ 0
⊢ rayOfNeZero R x hx✝ = Basis.orientation e ∨ rayOfNeZero R x hx✝ = -Basis.orientation e
case h
R : Type u_2
inst✝⁴ : LinearOrderedCommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
x : AlternatingMap R M R ι
hx : x ≠ 0
⊢ rayOfNeZero R x hx = Basis.orientation e ∨ rayOfNeZero R x hx = -Basis.orientation e
rw [← x.map_basis_ne_zero_iff e] at hx
no goals
case h
R : Type u_2
inst✝⁴ : LinearOrderedCommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
x : AlternatingMap R M R ι
hx✝ : x ≠ 0
hx : ↑x ↑e ≠ 0
⊢ rayOfNeZero R x hx✝ = Basis.orientation e ∨ rayOfNeZero R x hx✝ = -Basis.orientation e
rwa [Basis.orientation, ray_eq_iff, neg_rayOfNeZero, ray_eq_iff, x.eq_smul_basis_det e,
  sameRay_neg_smul_left_iff_of_ne e.det_ne_zero hx, sameRay_smul_left_iff_of_ne e.det_ne_zero hx,
  lt_or_lt_iff_ne, ne_comm]