Documentation Verification Report

Lemmas

📁 Source: FLT/Deformations/Lemmas.lean

Statistics

Metric	Count
Definitions `instDistrbMulAction`, `map`, `ofIsModuleTopology`, `mapMatrix`, `toContinuousMonoidHom`, `toHomUnits`, `endSelf`, `coeHomₜ`, `mapₜ`, `instAlgebraSubtypeMemValuationSubring_fLT`, `instMulActionContinuousMonoidHomOfContinuousConstSMul_fLT`, `instMulActionMonoidHomOfMulDistribMulAction_fLT`, `instMulSemiringActionRingOfIntegers_fLT`, `instMulSemiringActionSubtypeMemIntermediateFieldOfSMulCommClassOfNormal_fLT`	14
Theorems `continuous_iff_isOpen_ker`, `map_algebraMap`, `coe_toContinuousMonoidHom`, `isLocalHom_comp`, `isLocalHom_id`, `isLocalHom_toRingHom`, `mapMatrix_apply`, `coe_mk`, `coe_smul`, `mk_toMonoidHom`, `val_inv_toHomUnits_toFun`, `val_toHomUnits_toFun`, `adjoin_adjoin_right`, `smulCommClass_of_normal`, `exists_ideal_isMaximal_and_isOpen`, `map_surjective`, `map_maximalIdeal`, `continuous_det`, `discreteUniformity`, `discreteUniformity`, `totallyBounded`, `coe_smul`, `continuous_iff_isOpen_ker`, `continuous_iff_isOpen_ker`, `index_op`, `algebraMap_def`, `coeHomₜ_toFun`, `val_inv_mapₜ_toFun`, `val_mapₜ_toFun`, `smulCommClass`, `continuousAt_discrete_rng`, `instContinuousConstSMulConjActOfContinuousMul_fLT`, `instFaithfulSMulSubtypeMemValuationSubring_fLT`, `instFiniteIndexMulOppositeOp_fLT`, `instIsLocalHomContinuousAlgHomToContinuousAlgHom_fLT`, `instIsLocalHomResidueFieldRingHomAlgebraMap_fLT`, `instIsLocalHomRingHomAlgebraMap_fLT`, `instIsLocalHomRingHomOfContinuousAlgHom_fLT`, `instIsLocalHomRingHomOfContinuousAlgHom_fLT_1`, `instIsLocalHomRingHomToRingHom_fLT`, `instIsLocalHomRingHomToRingHom_fLT_1`, `instIsModuleTopologyMatrixOfFiniteOfIsTopologicalRing_fLT`, `instNumberFieldSubtypeMemIntermediateFieldOfFiniteDimensional_fLT`	43
Total	57

AddMonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_iff_isOpen_ker` 📖	—	—	—	—	—

Additive

Definitions

Name	Category	Theorems
`instDistrbMulAction` 📖	CompOp	—

AlgebraicClosure

Definitions

Name	Category	Theorems
`map` 📖	CompOp	2 math math: `map_algebraMap`, `Field.absoluteGaloisGroup.lift_map`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_algebraMap` 📖	mathematical	—	`map`	—	—

ContinuousAlgEquiv

Definitions

Name	Category	Theorems
`ofIsModuleTopology` 📖	CompOp	—

ContinuousAlgHom

Definitions

Name	Category	Theorems
`mapMatrix` 📖	CompOp	1 math math: `mapMatrix_apply`
`toContinuousMonoidHom` 📖	CompOp	1 math math: `coe_toContinuousMonoidHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_toContinuousMonoidHom` 📖	mathematical	—	`toContinuousMonoidHom`	—	—
`isLocalHom_comp` 📖	—	—	—	—	`instIsLocalHomRingHomOfContinuousAlgHom_fLT_1`
`isLocalHom_id` 📖	—	—	—	—	—
`isLocalHom_toRingHom` 📖	—	—	—	—	—
`mapMatrix_apply` 📖	mathematical	—	`mapMatrix`	—	—

ContinuousMonoidHom

Definitions

Name	Category	Theorems
`toHomUnits` 📖	CompOp	2 math math: `val_inv_toHomUnits_toFun`, `val_toHomUnits_toFun`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_mk` 📖	—	—	—	—	—
`coe_smul` 📖	mathematical	—	`instMulActionContinuousMonoidHomOfContinuousConstSMul_fLT`	—	—
`mk_toMonoidHom` 📖	—	—	—	—	—
`val_inv_toHomUnits_toFun` 📖	mathematical	—	`toHomUnits`	—	—
`val_toHomUnits_toFun` 📖	mathematical	—	`toHomUnits`	—	—

IntermediateField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjoin_adjoin_right` 📖	—	—	—	—	—
`smulCommClass_of_normal` 📖	mathematical	—	`instMulSemiringActionSubtypeMemIntermediateFieldOfSMulCommClassOfNormal_fLT`	—	—

IsLinearTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_ideal_isMaximal_and_isOpen` 📖	—	—	—	—	—

IsLocalRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_maximalIdeal` 📖	—	—	—	—	—

IsLocalRing.ResidueField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_surjective` 📖	—	—	—	—	—

IsModuleTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_det` 📖	—	—	—	—	—

IsTopologicalAddGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`discreteUniformity` 📖	—	—	—	—	—

IsTopologicalGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`discreteUniformity` 📖	—	—	—	—	—
`totallyBounded` 📖	—	—	—	—	`instFiniteIndexMulOppositeOp_fLT`

Module

Definitions

Name	Category	Theorems
`endSelf` 📖	CompOp	—

MonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_smul` 📖	mathematical	—	`instMulActionMonoidHomOfMulDistribMulAction_fLT`	—	—
`continuous_iff_isOpen_ker` 📖	—	—	—	—	—

RingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_iff_isOpen_ker` 📖	—	—	—	—	`AddMonoidHom.continuous_iff_isOpen_ker`

Subgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`index_op` 📖	—	—	—	—	—

Subring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap_def` 📖	—	—	—	—	—

Units

Definitions

Name	Category	Theorems
`coeHomₜ` 📖	CompOp	1 math math: `coeHomₜ_toFun`
`mapₜ` 📖	CompOp	2 math math: `val_mapₜ_toFun`, `val_inv_mapₜ_toFun`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeHomₜ_toFun` 📖	mathematical	—	`coeHomₜ`	—	—
`val_inv_mapₜ_toFun` 📖	mathematical	—	`mapₜ`	—	—
`val_mapₜ_toFun` 📖	mathematical	—	`mapₜ`	—	—

ValuationSubring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smulCommClass` 📖	mathematical	—	`instAlgebraSubtypeMemValuationSubring_fLT`	—	—

(root)

Definitions

Name	Category	Theorems
`instAlgebraSubtypeMemValuationSubring_fLT` 📖	CompOp	6 math math: `neZero_maximalIdeal_integralClosure`, `Field.AbsoluteGaloisGroup.isArithFrobAt_adicArithFrob`, `not_isField_integralClosure`, `ValuationSubring.smulCommClass`, `valuationRing_integralClosure`, `isInvariant_integralClosure`
`instMulActionContinuousMonoidHomOfContinuousConstSMul_fLT` 📖	CompOp	1 math math: `ContinuousMonoidHom.coe_smul`
`instMulActionMonoidHomOfMulDistribMulAction_fLT` 📖	CompOp	1 math math: `MonoidHom.coe_smul`
`instMulSemiringActionRingOfIntegers_fLT` 📖	CompOp	—
`instMulSemiringActionSubtypeMemIntermediateFieldOfSMulCommClassOfNormal_fLT` 📖	CompOp	1 math math: `IntermediateField.smulCommClass_of_normal`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousAt_discrete_rng` 📖	—	—	—	—	—
`instContinuousConstSMulConjActOfContinuousMul_fLT` 📖	—	—	—	—	—
`instFaithfulSMulSubtypeMemValuationSubring_fLT` 📖	—	—	—	—	—
`instFiniteIndexMulOppositeOp_fLT` 📖	—	—	—	—	`Subgroup.index_op`
`instIsLocalHomContinuousAlgHomToContinuousAlgHom_fLT` 📖	—	—	—	—	—
`instIsLocalHomResidueFieldRingHomAlgebraMap_fLT` 📖	—	—	—	—	—
`instIsLocalHomRingHomAlgebraMap_fLT` 📖	—	—	—	—	—
`instIsLocalHomRingHomOfContinuousAlgHom_fLT` 📖	—	—	—	—	`ContinuousAlgHom.isLocalHom_toRingHom`
`instIsLocalHomRingHomOfContinuousAlgHom_fLT_1` 📖	—	—	—	—	`ContinuousAlgHom.isLocalHom_toRingHom`
`instIsLocalHomRingHomToRingHom_fLT` 📖	—	—	—	—	—
`instIsLocalHomRingHomToRingHom_fLT_1` 📖	—	—	—	—	—
`instIsModuleTopologyMatrixOfFiniteOfIsTopologicalRing_fLT` 📖	—	—	—	—	—
`instNumberFieldSubtypeMemIntermediateFieldOfFiniteDimensional_fLT` 📖	—	—	—	—	—

---

← Back to Index