Def Vector3.ofFn

Modification history

2024-05-07 01:05

Mathlib/Data/Vector3.lean

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

Deleted Vector3.ofFn View on Github →

2023-06-09 04:21

Mathlib/Data/Vector3.lean

feat: port Data.Vector3 (#1204)

Added Vector3.ofFn View on Github →