Theorem Int.ofNat_bit1

Modification history

2024-07-12 11:12
Mathlib/Data/Int/Defs.lean
chore: remove unused lemmas about bit0/1 (#14672)
Deleted Int.ofNat_bit1View on Github →
2024-06-15 14:58
Mathlib/Data/Int/Defs.lean
chore(*): more `since :=` in `deprecated` (#13839)
Modified Int.ofNat_bit1View on Github →
2024-01-06 09:51
Mathlib/Data/Int/Cast/Basic.lean
refactor: Split off basic `Int` file (#9443) …
Modified Int.ofNat_bit1View on Github →
2022-11-23 03:12
Mathlib/Data/Int/Cast/Basic.lean
feat: port Data.Int.Cast.Basic (#670) …
Added Int.ofNat_bit1View on Github →