PadicIntegers

📁 Source: FLT/Mathlib/NumberTheory/Padics/PadicIntegers.lean

Statistics

Metric	Count
Definitions instCoeSubtypeMemSubmonoidNonZeroDivisorsUnitsPadic_fLT, instCoeUnitsPadic_fLT	2
Theorems comap_smul_one, submodule_one_eq_closedBall, closure_nonZeroDivisors_padicInt, coe_coeRingHom, coe_inj, coe_injective, exists_unit_mul_p_pow_eq, image_coe_smul_set, index_span_p_pow, instInfinite_fLT, nnnorm_p, nnnorm_units, smul_submodule_one_index, smul_submodule_one_isFiniteRelIndex, smul_submodule_one_relIndex	15
Total	17

AddSubgroup

Theorems

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

Padic

Theorems

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

PadicInt

Definitions

Name	Category	Theorems
instCoeSubtypeMemSubmonoidNonZeroDivisorsUnitsPadic_fLT 📖	CompOp	—
instCoeUnitsPadic_fLT 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_nonZeroDivisors_padicInt 📖	—	—	—	—	—
coe_coeRingHom 📖	—	—	—	—	—
coe_inj 📖	—	—	—	—	coe_injective
coe_injective 📖	—	—	—	—	—
exists_unit_mul_p_pow_eq 📖	—	—	—	—	—
image_coe_smul_set 📖	—	—	—	—	—
index_span_p_pow 📖	—	—	—	—	—
instInfinite_fLT 📖	—	—	—	—	—
nnnorm_p 📖	—	—	—	—	—
nnnorm_units 📖	—	—	—	—	—
smul_submodule_one_index 📖	—	—	—	—	instInfinite_fLT index_span_p_pow
smul_submodule_one_isFiniteRelIndex 📖	—	—	—	—	smul_submodule_one_relIndex
smul_submodule_one_relIndex 📖	—	—	—	—	smul_submodule_one_index AddSubgroup.comap_smul_one

---

← Back to Index