Documentation Verification Report

IntermediateField

📁 Source: ClassFieldTheory/Mathlib/FieldTheory/Finite/IntermediateField.lean

Statistics

Metric	Count
Definitions `intermediateField`	1
Theorems `adjoin_eq_intermediateField_of_isPrimitiveRoot`, `degree_minpoly_of_isPrimitiveRoot`, `instHasEnoughRootsOfUnityHSubNatCardOfNat_classFieldTheory`, `intermediateField_eq_insert_zero_nthRootsFinset_one`, `intermediateField_eq_rootSet`, `mem_intermediateField_iff`, `mem_intermediateField_iff'`, `rootsOfUnity_eq_top`	8
Total	9

FiniteField

Definitions

Name	Category	Theorems
`intermediateField` 📖	CompOp	5 math math: `mem_intermediateField_iff'`, `mem_intermediateField_iff`, `intermediateField_eq_insert_zero_nthRootsFinset_one`, `adjoin_eq_intermediateField_of_isPrimitiveRoot`, `intermediateField_eq_rootSet`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjoin_eq_intermediateField_of_isPrimitiveRoot` 📖	mathematical	—	`intermediateField`	—	`mem_intermediateField_iff'` `HasEnoughRootsOfUnity.exists_pow`
`degree_minpoly_of_isPrimitiveRoot` 📖	—	—	—	—	`adjoin_eq_intermediateField_of_isPrimitiveRoot` `intermediateField_eq_rootSet` `Polynomial.X_pow_sub_X_splits`
`instHasEnoughRootsOfUnityHSubNatCardOfNat_classFieldTheory` 📖	—	—	—	—	`rootsOfUnity_eq_top`
`intermediateField_eq_insert_zero_nthRootsFinset_one` 📖	mathematical	—	`intermediateField`	—	`mem_intermediateField_iff'`
`intermediateField_eq_rootSet` 📖	mathematical	—	`intermediateField`	—	—
`mem_intermediateField_iff` 📖	mathematical	—	`intermediateField`	—	—
`mem_intermediateField_iff'` 📖	mathematical	—	`intermediateField`	—	`mem_intermediateField_iff`
`rootsOfUnity_eq_top` 📖	—	—	—	—	—

---

← Back to Index