Actions

📁 Source: ClassFieldTheory/IsNonarchimedeanLocalField/Actions.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_units_mul_irreducible_zpow, instIsInvariantSubringAlgEquivIntegerValueGroupWithZeroValuation_classFieldTheory, invariant, valuation_algEquiv_apply, valuation_algHom_apply, valuation_smul, coe_inv₀	7
Total	7

IsNonarchimedeanLocalField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_units_mul_irreducible_zpow 📖	—	—	—	—	Units.coe_inv₀
instIsInvariantSubringAlgEquivIntegerValueGroupWithZeroValuation_classFieldTheory 📖	—	—	—	—	invariant
invariant 📖	—	—	—	—	valuation_smul
valuation_algEquiv_apply 📖	—	—	—	—	isIntegral_iff instIsScalarTowerSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory exists_units_mul_irreducible_zpow valuation_units_integer_eq_one valuation_irreducible
valuation_algHom_apply 📖	—	—	—	—	valuation_algEquiv_apply instFiniteDimensional_classFieldTheory
valuation_smul 📖	—	—	—	—	valuation_algHom_apply

Units

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_inv₀ 📖	—	—	—	—	—

---

← Back to Index