Size

📁 Source: Mathlib/Data/Nat/Size.lean

Statistics

Metric	Count
Definitions	0
Theorems lt_size, lt_size_self, shiftLeft'_ne_zero_left, shiftLeft'_tt_eq_mul_pow, shiftLeft'_tt_ne_zero, shiftLeft_eq_mul_pow, size_bit, size_eq_bits_len, size_eq_zero, size_le, size_le_size, size_one, size_pos, size_pow, size_shiftLeft, size_shiftLeft', size_zero	17
Total	17

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lt_size 📖	mathematical	—	size Monoid.toNatPow instMonoid	—	not_lt size_le
lt_size_self 📖	mathematical	—	Monoid.toNatPow instMonoid size	—	size_zero size_bit one_mul
shiftLeft'_ne_zero_left 📖	—	—	—	—	—
shiftLeft'_tt_eq_mul_pow 📖	mathematical	—	shiftLeft' Monoid.toNatPow instMonoid	—	pow_zero mul_one shiftLeft'.eq_2 bit_val add_assoc mul_left_comm mul_comm pow_succ
shiftLeft'_tt_ne_zero 📖	—	—	—	—	—
shiftLeft_eq_mul_pow 📖	mathematical	—	Monoid.toNatPow instMonoid	—	—
size_bit 📖	mathematical	—	size bit	—	binaryRec.eq_1 bit_shiftRight_one
size_eq_bits_len 📖	mathematical	—	bits size	—	zero_bits size_zero size_bit bits_append_bit
size_eq_zero 📖	mathematical	—	size	—	size_pos
size_le 📖	mathematical	—	size Monoid.toNatPow instMonoid	—	lt_of_lt_of_le lt_size_self size_zero size_bit lt_of_le_of_lt
size_le_size 📖	mathematical	—	size	—	size_le lt_of_le_of_lt lt_size_self
size_one 📖	mathematical	—	size	—	size_bit size_zero
size_pos 📖	mathematical	—	size	—	lt_size
size_pow 📖	mathematical	—	size Monoid.toNatPow instMonoid	—	le_antisymm size_le lt_size le_rfl
size_shiftLeft 📖	mathematical	—	size	—	size_shiftLeft' shiftLeft'_ne_zero_left
size_shiftLeft' 📖	mathematical	—	size shiftLeft'	—	add_zero size_bit not_ne_iff zero_add one_mul shiftLeft'_tt_eq_mul_pow
size_zero 📖	mathematical	—	size	—	—

---

← Back to Index