Basic

📁 Source: ClassFieldTheory/Mathlib/RingTheory/Valuation/Basic.lean

Statistics

Metric	Count
Definitions ball, closedBall, sphere	3
Theorems ball_eq_ball, closedBall_eq_closedBall, le_iff_le, sphere_eq_sphere, ext_lt_one, mem_ball_iff, mem_closedBall_iff, mem_sphere_iff, ne_zero_of_isUnit', ne_zero_of_unit'	10
Total	13

Valuation

Definitions

Name	Category	Theorems
ball 📖	CompOp	3 math math: mem_ball_iff, NormedField.valuation_ball_eq, IsEquiv.ball_eq_ball
closedBall 📖	CompOp	2 math math: mem_closedBall_iff, IsEquiv.closedBall_eq_closedBall
sphere 📖	CompOp	2 math math: mem_sphere_iff, IsEquiv.sphere_eq_sphere

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext_lt_one 📖	—	—	—	—	—
mem_ball_iff 📖	mathematical	—	ball	—	—
mem_closedBall_iff 📖	mathematical	—	closedBall	—	—
mem_sphere_iff 📖	mathematical	—	sphere	—	—
ne_zero_of_isUnit' 📖	—	—	—	—	ne_zero_of_unit'
ne_zero_of_unit' 📖	—	—	—	—	—

Valuation.IsEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ball_eq_ball 📖	mathematical	—	Valuation.ball	—	—
closedBall_eq_closedBall 📖	mathematical	—	Valuation.closedBall	—	le_iff_le
le_iff_le 📖	—	—	—	—	—
sphere_eq_sphere 📖	mathematical	—	Valuation.sphere	—	—

---

← Back to Index