Def Vector3.nth

Modification history

2024-05-07 01:05

Mathlib/Data/Vector3.lean

refactor: replace `@[reducible]` with `abbrev` (#12614) …

Deleted Vector3.nth View on Github →

2023-06-09 04:21

Mathlib/Data/Vector3.lean

feat: port Data.Vector3 (#1204)

Added Vector3.nth View on Github →