Mathlib v3 is deprecated. Go to Mathlib v4

Theorem star_nat_cast

Modification history

2022-03-03 21:31
src/algebra/star/basic.lean
feat(data/{nat,int,rat}/cast, algebra/star/basic): lemmas about `star` on casts (#12418) …
Added star_nat_castView on Github →