Theorem Module.Ray.units_smul_of_pos

Modification history

2025-04-03 04:39

Mathlib/LinearAlgebra/Ray.lean

chore(LinearAlgebra/*): process misc porting notes (#23551)

Modified Module.Ray.units_smul_of_pos View on Github →

2023-02-27 13:07

Mathlib/LinearAlgebra/Ray.lean

feat: port LinearAlgebra.Ray (#2468)

Added Module.Ray.units_smul_of_pos View on Github →