Mathlib v3 is deprecated. Go to Mathlib v4

Theorem smul_two

Modification history

2018-04-03 21:23
algebra/group_power.lean
fix(*): update to lean …
Deleted smul_twoView on Github →
2018-01-21 23:57
algebra/group_power.lean
feat(data/real): real square root function, sqrt 2 is irrational
Added smul_twoView on Github →