Def Vector3.unexpandNil

Modification history

2025-11-19 06:07

Mathlib/Data/Vector3.lean

chore: move Mathlib to the module system (#31786) …

Deleted Vector3.unexpandNil View on Github →

2023-06-09 04:21

Mathlib/Data/Vector3.lean

feat: port Data.Vector3 (#1204)

Added Vector3.unexpandNil View on Github →