WeakApproximation

📁 Source: FLT/NumberField/InfinitePlace/WeakApproximation.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_one_lt_lt_one, exists_one_lt_lt_one_lt_one_of_eq_one, exists_one_lt_lt_one_lt_one_of_one_lt, exists_tendsto_const_tendsto_zero_tendsto_const, exists_tendsto_zero_tendsto_atTop_tendsto_const, denseRange_algebraMap_subtype_pi, eq_of_eq_rpow, exists_one_lt_lt_one, exists_tendsto_one_tendsto_zero, pos_of_pos, rpow_eq_one_of_eq_rpow	11
Total	11

AbsoluteValue

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_one_lt_lt_one 📖	—	—	—	—	exists_one_lt_lt_one_of_ne_rpow Fin.pairwise_forall_two exists_one_lt_lt_one_lt_one_of_eq_one exists_one_lt_lt_one_lt_one_of_one_lt
exists_one_lt_lt_one_lt_one_of_eq_one 📖	—	—	—	—	exists_tendsto_zero_tendsto_atTop_tendsto_const
exists_one_lt_lt_one_lt_one_of_one_lt 📖	—	—	—	—	exists_tendsto_const_tendsto_zero_tendsto_const
exists_tendsto_const_tendsto_zero_tendsto_const 📖	—	—	—	—	pos_of_pos
exists_tendsto_zero_tendsto_atTop_tendsto_const 📖	—	—	—	—	—

NumberField.InfinitePlace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_of_eq_rpow 📖	—	—	—	—	rpow_eq_one_of_eq_rpow
exists_one_lt_lt_one 📖	—	—	—	—	AbsoluteValue.exists_one_lt_lt_one eq_of_eq_rpow
exists_tendsto_one_tendsto_zero 📖	—	—	—	—	pos_of_pos
pos_of_pos 📖	—	—	—	—	AbsoluteValue.pos_of_pos
rpow_eq_one_of_eq_rpow 📖	—	—	—	—	—

NumberField.InfinitePlace.Completion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
denseRange_algebraMap_subtype_pi 📖	—	—	—	—	—

---

← Back to Index