FLT/Mathlib/RingTheory/
96 declarations, 0 contain sorry, 0 declared as axioms; 21 files
Folders
- DedekindDomain/ 3 files, 30 declarations
- DiscreteValuationRing/ 2 files, 12 declarations
- Ideal/ 1 files, 1 declarations
- LocalRing/ 2 files, 3 declarations
- Localization/ 1 files, 6 declarations
- Norm/ 2 files, 10 declarations
- Polynomial/ 1 files, 1 declarations
- RamificationInertia/ 1 files, 1 declarations
- SimpleRing/ 1 files, 8 declarations
- TensorProduct/ 2 files, 5 declarations
- Unramified/ 1 files, 1 declarations
- Valuation/ 3 files, 13 declarations
Files
- AdjoinRoot.lean 5 declarations