Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

Commit

Permalink
fix(linear_algebra/affine_space/affine_subspace): remove obsolete com…
Browse files Browse the repository at this point in the history
…ment (#17586)

This comment is no longer needed after notations for norms and "parallel" were fixed.
  • Loading branch information
jsm28 committed Nov 17, 2022
1 parent 8ab239e commit ee768c0
Showing 1 changed file with 0 additions and 3 deletions.
3 changes: 0 additions & 3 deletions src/linear_algebra/affine_space/affine_subspace.lean
Original file line number Diff line number Diff line change
Expand Up @@ -1548,9 +1548,6 @@ to all points. -/
def parallel (s₁ s₂ : affine_subspace k P) : Prop :=
∃ v : V, s₂ = s₁.map (const_vadd k P v)

/- The notation should logically be U+2225 PARALLEL TO, but that is used globally for norms at
present, and norms and parallelism are both widely used in geometry, so use U+2016 DOUBLE
VERTICAL LINE (which is logically more appropriate for norms) instead here to avoid conflict. -/
localized "infix (name := affine_subspace.parallel) ` ∥ `:50 := affine_subspace.parallel" in affine

@[symm] lemma parallel.symm {s₁ s₂ : affine_subspace k P} (h : s₁ ∥ s₂) : s₂ ∥ s₁ :=
Expand Down

0 comments on commit ee768c0

Please sign in to comment.