Documentation Verification Report

IntegralClosure

📁 Source: FLT/Deformations/RepresentationTheory/IntegralClosure.lean

Statistics

Metric	Count
Definitions `IntegralClosure`, `instAlgebraIntegralClosure`, `instAlgebraIntegralClosure_1`, `instCommRingIntegralClosure`, `mulSemiringActionIntegralClosure`	5
Theorems `continuousSMulDiscrete_integralClosure`, `instFaithfulSMulIntegralClosure`, `instIsDomainIntegralClosure`, `instIsIntegralIntegralClosure`, `instIsScalarTowerIntegralClosure`, `instNeZeroIdealUnderOfNontrivialOfIsDomainOfIsIntegral_fLT`, `isInvariant_integralClosure`, `not_isField_integralClosure`, `smulCommClass_integralClosure`	9
Total	14

(root)

Definitions

Name	Category	Theorems
`IntegralClosure` 📖	CompOp	11 math math: `neZero_maximalIdeal_integralClosure`, `instIsScalarTowerIntegralClosure`, `instIsIntegralIntegralClosure`, `Field.AbsoluteGaloisGroup.isArithFrobAt_adicArithFrob`, `instIsDomainIntegralClosure`, `not_isField_integralClosure`, `instFaithfulSMulIntegralClosure`, `valuationRing_integralClosure`, `isInvariant_integralClosure`, `continuousSMulDiscrete_integralClosure`, `smulCommClass_integralClosure`
`instAlgebraIntegralClosure` 📖	CompOp	6 math math: `instIsScalarTowerIntegralClosure`, `instIsIntegralIntegralClosure`, `Field.AbsoluteGaloisGroup.isArithFrobAt_adicArithFrob`, `instFaithfulSMulIntegralClosure`, `isInvariant_integralClosure`, `smulCommClass_integralClosure`
`instAlgebraIntegralClosure_1` 📖	CompOp	1 math math: `instIsScalarTowerIntegralClosure`
`instCommRingIntegralClosure` 📖	CompOp	11 math math: `neZero_maximalIdeal_integralClosure`, `instIsScalarTowerIntegralClosure`, `instIsIntegralIntegralClosure`, `Field.AbsoluteGaloisGroup.isArithFrobAt_adicArithFrob`, `instIsDomainIntegralClosure`, `not_isField_integralClosure`, `instFaithfulSMulIntegralClosure`, `valuationRing_integralClosure`, `isInvariant_integralClosure`, `continuousSMulDiscrete_integralClosure`, `smulCommClass_integralClosure`
`mulSemiringActionIntegralClosure` 📖	CompOp	4 math math: `Field.AbsoluteGaloisGroup.isArithFrobAt_adicArithFrob`, `isInvariant_integralClosure`, `continuousSMulDiscrete_integralClosure`, `smulCommClass_integralClosure`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousSMulDiscrete_integralClosure` 📖	mathematical	—	`ContinuousSMulDiscrete` `IntegralClosure` `instCommRingIntegralClosure` `mulSemiringActionIntegralClosure`	—	`ContinuousSMulDiscrete.isOpen_smul_eq`
`instFaithfulSMulIntegralClosure` 📖	mathematical	—	`IntegralClosure` `instCommRingIntegralClosure` `instAlgebraIntegralClosure`	—	—
`instIsDomainIntegralClosure` 📖	mathematical	—	`IntegralClosure` `instCommRingIntegralClosure`	—	—
`instIsIntegralIntegralClosure` 📖	mathematical	—	`IntegralClosure` `instCommRingIntegralClosure` `instAlgebraIntegralClosure`	—	—
`instIsScalarTowerIntegralClosure` 📖	mathematical	—	`IntegralClosure` `instCommRingIntegralClosure` `instAlgebraIntegralClosure` `instAlgebraIntegralClosure_1`	—	—
`instNeZeroIdealUnderOfNontrivialOfIsDomainOfIsIntegral_fLT` 📖	—	—	—	—	—
`isInvariant_integralClosure` 📖	mathematical	—	`IntegralClosure` `instAlgebraSubtypeMemValuationSubring_fLT` `instCommRingIntegralClosure` `instAlgebraIntegralClosure` `mulSemiringActionIntegralClosure` `ValuationSubring.smulCommClass`	—	`ValuationSubring.smulCommClass`
`not_isField_integralClosure` 📖	mathematical	—	`IntegralClosure` `instAlgebraSubtypeMemValuationSubring_fLT` `instCommRingIntegralClosure`	—	`instFaithfulSMulIntegralClosure` `instFaithfulSMulSubtypeMemValuationSubring_fLT` `instIsIntegralIntegralClosure`
`smulCommClass_integralClosure` 📖	mathematical	—	`IntegralClosure` `instCommRingIntegralClosure` `mulSemiringActionIntegralClosure` `instAlgebraIntegralClosure`	—	—

---

← Back to Index