|
ClassFieldTheory/Cohomology/AugmentationModule.lean |
8 |
19 |
|
|
ClassFieldTheory/Cohomology/FiniteCyclic/ExplicitTate.lean |
11 |
4 |
|
|
ClassFieldTheory/Cohomology/FiniteCyclic/HerbrandQuotient/Defs.lean |
2 |
4 |
|
|
ClassFieldTheory/Cohomology/FiniteCyclic/HerbrandQuotient/Finite.lean |
0 |
2 |
|
|
ClassFieldTheory/Cohomology/FiniteCyclic/HerbrandQuotient/SES.lean |
1 |
5 |
|
|
ClassFieldTheory/Cohomology/FiniteCyclic/HerbrandQuotient/Trivial.lean |
2 |
8 |
|
|
ClassFieldTheory/Cohomology/FiniteCyclic/UpDown.lean |
16 |
40 |
|
|
ClassFieldTheory/Cohomology/Functors/Corestriction.lean |
5 |
16 |
|
|
ClassFieldTheory/Cohomology/Functors/Inflation.lean |
5 |
8 |
|
|
ClassFieldTheory/Cohomology/Functors/InflationRestriction.lean |
1 |
3 |
3 |
|
ClassFieldTheory/Cohomology/Functors/Restriction.lean |
8 |
26 |
|
|
ClassFieldTheory/Cohomology/Functors/UpDown.lean |
20 |
39 |
2 |
|
ClassFieldTheory/Cohomology/IndCoind/Finite.lean |
39 |
41 |
|
|
ClassFieldTheory/Cohomology/IndCoind/TrivialCohomology.lean |
5 |
23 |
|
|
ClassFieldTheory/Cohomology/IsFilterComplete/Basic.lean |
18 |
30 |
|
|
ClassFieldTheory/Cohomology/IsFilterComplete/Forget.lean |
0 |
1 |
|
|
ClassFieldTheory/Cohomology/IsFilterComplete/Submodule.lean |
1 |
11 |
|
|
ClassFieldTheory/Cohomology/LeftRegular.lean |
5 |
10 |
|
|
ClassFieldTheory/Cohomology/LocalInv.lean |
7 |
13 |
|
|
ClassFieldTheory/Cohomology/SerreApproximation.lean |
8 |
37 |
|
|
ClassFieldTheory/Cohomology/SplittingModule.lean |
14 |
28 |
|
|
ClassFieldTheory/Cohomology/Subrep/Basic.lean |
17 |
9 |
|
|
ClassFieldTheory/Cohomology/Subrep/ShortExact.lean |
3 |
2 |
|
|
ClassFieldTheory/Cohomology/TateCohomology.lean |
24 |
59 |
|
|
ClassFieldTheory/Cohomology/TrivialCohomology.lean |
4 |
25 |
|
|
ClassFieldTheory/Cohomology/TrivialityCriterion.lean |
0 |
6 |
|
|
ClassFieldTheory/IsNonarchimedeanLocalField/Actions.lean |
0 |
7 |
|
|
ClassFieldTheory/IsNonarchimedeanLocalField/Adic.lean |
0 |
3 |
|
|
ClassFieldTheory/IsNonarchimedeanLocalField/Basic.lean |
10 |
56 |
4 |
|
ClassFieldTheory/IsNonarchimedeanLocalField/HerbrandQuotient.lean |
0 |
2 |
1 |
|
ClassFieldTheory/IsNonarchimedeanLocalField/Instances.lean |
3 |
3 |
2 |
|
ClassFieldTheory/IsNonarchimedeanLocalField/IntermediateField.lean |
0 |
1 |
|
|
ClassFieldTheory/IsNonarchimedeanLocalField/RamificationInertia.lean |
0 |
23 |
|
|
ClassFieldTheory/IsNonarchimedeanLocalField/Tower.lean |
0 |
1 |
|
|
ClassFieldTheory/IsNonarchimedeanLocalField/Unramified.lean |
7 |
27 |
|
|
ClassFieldTheory/IsNonarchimedeanLocalField/UnramifiedCohomology.lean |
0 |
1 |
1 |
|
ClassFieldTheory/IsNonarchimedeanLocalField/Valuation.lean |
3 |
11 |
|
|
ClassFieldTheory/IsNonarchimedeanLocalField/ValuationExactSequence.lean |
3 |
16 |
|
|
ClassFieldTheory/LocalCFT/Continuity.lean |
0 |
5 |
|
|
ClassFieldTheory/LocalCFT/Teichmuller.lean |
3 |
27 |
|
|
ClassFieldTheory/Mathlib/Algebra/Group/Solvable.lean |
0 |
3 |
|
|
ClassFieldTheory/Mathlib/Algebra/Group/Units/Defs.lean |
0 |
1 |
|
|
ClassFieldTheory/Mathlib/Algebra/Group/Units/Hom.lean |
0 |
1 |
|
|
ClassFieldTheory/Mathlib/Algebra/Homology/ConcreteCategory.lean |
0 |
1 |
|
|
ClassFieldTheory/Mathlib/Algebra/Homology/ShortComplex/ConcreteCategory.lean |
0 |
1 |
|
|
ClassFieldTheory/Mathlib/Algebra/Homology/ShortComplex/Exact.lean |
2 |
4 |
|
|
ClassFieldTheory/Mathlib/Algebra/Homology/ShortComplex/ModuleCat.lean |
0 |
3 |
|
|
ClassFieldTheory/Mathlib/Algebra/Homology/ShortComplex/Rep.lean |
1 |
5 |
|
|
ClassFieldTheory/Mathlib/Algebra/Homology/ShortComplex/ShortExact.lean |
0 |
2 |
|
|
ClassFieldTheory/Mathlib/Algebra/Module/Torsion/Basic.lean |
1 |
2 |
|
|
ClassFieldTheory/Mathlib/Algebra/Order/Group/OrderIso.lean |
0 |
1 |
|
|
ClassFieldTheory/Mathlib/Algebra/Order/GroupWithZero/Canonical.lean |
0 |
6 |
|
|
ClassFieldTheory/Mathlib/Algebra/Order/Hom/Monoid.lean |
0 |
5 |
|
|
ClassFieldTheory/Mathlib/CategoryTheory/Category/Basic.lean |
0 |
1 |
|
|
ClassFieldTheory/Mathlib/CategoryTheory/Category/Cat.lean |
0 |
1 |
|
|
ClassFieldTheory/Mathlib/Data/Finsupp/Single.lean |
0 |
2 |
|
|
ClassFieldTheory/Mathlib/Data/Int/WithZero.lean |
0 |
1 |
|
|
ClassFieldTheory/Mathlib/FieldTheory/Finite/Basic.lean |
0 |
1 |
|
|
ClassFieldTheory/Mathlib/FieldTheory/Finite/IntermediateField.lean |
1 |
8 |
|
|
ClassFieldTheory/Mathlib/FieldTheory/Separable.lean |
0 |
3 |
|
|
ClassFieldTheory/Mathlib/GroupTheory/GroupAction/Quotient.lean |
0 |
1 |
|
|
ClassFieldTheory/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean |
1 |
3 |
|
|
ClassFieldTheory/Mathlib/GroupTheory/Torsion.lean |
0 |
5 |
|
|
ClassFieldTheory/Mathlib/LinearAlgebra/Finsupp/Defs.lean |
0 |
2 |
|
|
ClassFieldTheory/Mathlib/LinearAlgebra/Isomorphisms.lean |
0 |
1 |
|
|
ClassFieldTheory/Mathlib/LinearAlgebra/Quotient/Card.lean |
0 |
2 |
|
|
ClassFieldTheory/Mathlib/Order/Filter/Bases/Monotone.lean |
0 |
2 |
|
|
ClassFieldTheory/Mathlib/RepresentationTheory/Basic.lean |
0 |
1 |
|
|
ClassFieldTheory/Mathlib/RepresentationTheory/Homological/GroupCohomology/Basic.lean |
0 |
1 |
|
|
ClassFieldTheory/Mathlib/RepresentationTheory/Homological/GroupCohomology/Functoriality.lean |
1 |
4 |
|
|
ClassFieldTheory/Mathlib/RepresentationTheory/Homological/GroupCohomology/LongExactSequence.lean |
0 |
2 |
|
|
ClassFieldTheory/Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean |
0 |
7 |
|
|
ClassFieldTheory/Mathlib/RepresentationTheory/Homological/GroupHomology/Functoriality.lean |
1 |
4 |
|
|
ClassFieldTheory/Mathlib/RepresentationTheory/Homological/GroupHomology/LongExactSequence.lean |
0 |
1 |
|
|
ClassFieldTheory/Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean |
1 |
4 |
|
|
ClassFieldTheory/Mathlib/RepresentationTheory/Invariants.lean |
2 |
4 |
|
|
ClassFieldTheory/Mathlib/RepresentationTheory/Rep.lean |
3 |
41 |
|
|
ClassFieldTheory/Mathlib/RingTheory/AdicCompletion/Ring.lean |
1 |
6 |
|
|
ClassFieldTheory/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean |
0 |
1 |
|
|
ClassFieldTheory/Mathlib/RingTheory/DiscreteValuationRing/Basic.lean |
0 |
3 |
|
|
ClassFieldTheory/Mathlib/RingTheory/HenselPolynomial.lean |
23 |
99 |
|
|
ClassFieldTheory/Mathlib/RingTheory/Ideal/Maps.lean |
0 |
1 |
|
|
ClassFieldTheory/Mathlib/RingTheory/LiftingCoprime.lean |
0 |
2 |
|
|
ClassFieldTheory/Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean |
1 |
0 |
|
|
ClassFieldTheory/Mathlib/RingTheory/Localization/AtPrime/Basic.lean |
0 |
1 |
|
|
ClassFieldTheory/Mathlib/RingTheory/Nilpotent/Lemmas.lean |
0 |
1 |
|
|
ClassFieldTheory/Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean |
0 |
2 |
|
|
ClassFieldTheory/Mathlib/RingTheory/RootsOfUnity/Basic.lean |
0 |
1 |
|
|
ClassFieldTheory/Mathlib/RingTheory/RootsOfUnity/EnoughRootsOfUnity.lean |
0 |
2 |
|
|
ClassFieldTheory/Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean |
0 |
4 |
|
|
ClassFieldTheory/Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean |
0 |
2 |
|
|
ClassFieldTheory/Mathlib/RingTheory/Unramified/Basic.lean |
0 |
1 |
|
|
ClassFieldTheory/Mathlib/RingTheory/Unramified/LocalRing.lean |
0 |
1 |
|
|
ClassFieldTheory/Mathlib/RingTheory/Valuation/Basic.lean |
3 |
10 |
|
|
ClassFieldTheory/Mathlib/RingTheory/Valuation/Integers.lean |
0 |
2 |
|
|
ClassFieldTheory/Mathlib/RingTheory/Valuation/ValuativeRel.lean |
1 |
15 |
|
|
ClassFieldTheory/Mathlib/SetTheory/Cardinal/Finite.lean |
0 |
1 |
|
|
ClassFieldTheory/Mathlib/Topology/Algebra/Group/Basic.lean |
0 |
2 |
|
|
ClassFieldTheory/Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean |
0 |
1 |
|
|
ClassFieldTheory/Mathlib/Topology/Algebra/Module/FiniteDimension.lean |
0 |
1 |
|
|
ClassFieldTheory/Mathlib/Topology/Algebra/Monoid.lean |
0 |
2 |
|
|
ClassFieldTheory/Mathlib/Topology/Algebra/Ring/Basic.lean |
0 |
2 |
|
|
ClassFieldTheory/Mathlib/Topology/Algebra/Valued/NormedValued.lean |
2 |
10 |
|
|
ClassFieldTheory/Mathlib/Topology/Algebra/Valued/ValuativeRel.lean |
0 |
4 |
|
|
ClassFieldTheory/Tactic/Dualize.lean |
2 |
0 |
|