Documentation
ClassFieldTheory
Search
return to top
source
Imports
Init
ClassFieldTheory.Cohomology.AugmentationModule
ClassFieldTheory.Cohomology.LeftRegular
ClassFieldTheory.Cohomology.LocalInv
ClassFieldTheory.Cohomology.SerreApproximation
ClassFieldTheory.Cohomology.SplittingModule
ClassFieldTheory.Cohomology.TateCohomology
ClassFieldTheory.Cohomology.TrivialCohomology
ClassFieldTheory.Cohomology.TrivialityCriterion
ClassFieldTheory.IsNonarchimedeanLocalField.Actions
ClassFieldTheory.IsNonarchimedeanLocalField.Adic
ClassFieldTheory.IsNonarchimedeanLocalField.Basic
ClassFieldTheory.IsNonarchimedeanLocalField.HerbrandQuotient
ClassFieldTheory.IsNonarchimedeanLocalField.Instances
ClassFieldTheory.IsNonarchimedeanLocalField.IntermediateField
ClassFieldTheory.IsNonarchimedeanLocalField.RamificationInertia
ClassFieldTheory.IsNonarchimedeanLocalField.Tower
ClassFieldTheory.IsNonarchimedeanLocalField.Unramified
ClassFieldTheory.IsNonarchimedeanLocalField.UnramifiedCohomology
ClassFieldTheory.IsNonarchimedeanLocalField.Valuation
ClassFieldTheory.IsNonarchimedeanLocalField.ValuationExactSequence
ClassFieldTheory.LocalCFT.Continuity
ClassFieldTheory.LocalCFT.Teichmuller
ClassFieldTheory.Tactic.Dualize
ClassFieldTheory.Cohomology.Examples.Examples
ClassFieldTheory.Cohomology.FiniteCyclic.ExplicitTate
ClassFieldTheory.Cohomology.FiniteCyclic.UpDown
ClassFieldTheory.Cohomology.Functors.Corestriction
ClassFieldTheory.Cohomology.Functors.Inflation
ClassFieldTheory.Cohomology.Functors.InflationRestriction
ClassFieldTheory.Cohomology.Functors.Restriction
ClassFieldTheory.Cohomology.Functors.UpDown
ClassFieldTheory.Cohomology.IndCoind.Finite
ClassFieldTheory.Cohomology.IndCoind.TrivialCohomology
ClassFieldTheory.Cohomology.IsFilterComplete.Basic
ClassFieldTheory.Cohomology.IsFilterComplete.Forget
ClassFieldTheory.Cohomology.IsFilterComplete.Submodule
ClassFieldTheory.Cohomology.Subrep.Basic
ClassFieldTheory.Cohomology.Subrep.ShortExact
ClassFieldTheory.Mathlib.FieldTheory.Separable
ClassFieldTheory.Mathlib.GroupTheory.Torsion
ClassFieldTheory.Mathlib.LinearAlgebra.Isomorphisms
ClassFieldTheory.Mathlib.RepresentationTheory.Basic
ClassFieldTheory.Mathlib.RepresentationTheory.Invariants
ClassFieldTheory.Mathlib.RepresentationTheory.Rep
ClassFieldTheory.Mathlib.RingTheory.HenselPolynomial
ClassFieldTheory.Mathlib.RingTheory.LiftingCoprime
ClassFieldTheory.Cohomology.FiniteCyclic.HerbrandQuotient.Defs
ClassFieldTheory.Cohomology.FiniteCyclic.HerbrandQuotient.Finite
ClassFieldTheory.Cohomology.FiniteCyclic.HerbrandQuotient.SES
ClassFieldTheory.Cohomology.FiniteCyclic.HerbrandQuotient.Trivial
ClassFieldTheory.Mathlib.Algebra.Group.Solvable
ClassFieldTheory.Mathlib.Algebra.Homology.ConcreteCategory
ClassFieldTheory.Mathlib.CategoryTheory.Category.Basic
ClassFieldTheory.Mathlib.CategoryTheory.Category.Cat
ClassFieldTheory.Mathlib.Data.Finsupp.Single
ClassFieldTheory.Mathlib.Data.Int.WithZero
ClassFieldTheory.Mathlib.FieldTheory.Finite.Basic
ClassFieldTheory.Mathlib.FieldTheory.Finite.IntermediateField
ClassFieldTheory.Mathlib.GroupTheory.GroupAction.Quotient
ClassFieldTheory.Mathlib.GroupTheory.SpecificGroups.Cyclic
ClassFieldTheory.Mathlib.LinearAlgebra.Finsupp.Defs
ClassFieldTheory.Mathlib.LinearAlgebra.Quotient.Card
ClassFieldTheory.Mathlib.RingTheory.AdicCompletion.Ring
ClassFieldTheory.Mathlib.RingTheory.DiscreteValuationRing.Basic
ClassFieldTheory.Mathlib.RingTheory.Ideal.Maps
ClassFieldTheory.Mathlib.RingTheory.Nilpotent.Lemmas
ClassFieldTheory.Mathlib.RingTheory.RootsOfUnity.Basic
ClassFieldTheory.Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
ClassFieldTheory.Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
ClassFieldTheory.Mathlib.RingTheory.UniqueFactorizationDomain.Basic
ClassFieldTheory.Mathlib.RingTheory.Unramified.Basic
ClassFieldTheory.Mathlib.RingTheory.Unramified.LocalRing
ClassFieldTheory.Mathlib.RingTheory.Valuation.Basic
ClassFieldTheory.Mathlib.RingTheory.Valuation.Integers
ClassFieldTheory.Mathlib.RingTheory.Valuation.ValuativeRel
ClassFieldTheory.Mathlib.SetTheory.Cardinal.Finite
ClassFieldTheory.Mathlib.Topology.Algebra.Monoid
ClassFieldTheory.Mathlib.Algebra.Group.Units.Defs
ClassFieldTheory.Mathlib.Algebra.Group.Units.Hom
ClassFieldTheory.Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory
ClassFieldTheory.Mathlib.Algebra.Homology.ShortComplex.Exact
ClassFieldTheory.Mathlib.Algebra.Homology.ShortComplex.ModuleCat
ClassFieldTheory.Mathlib.Algebra.Homology.ShortComplex.Rep
ClassFieldTheory.Mathlib.Algebra.Homology.ShortComplex.ShortExact
ClassFieldTheory.Mathlib.Algebra.Module.Torsion.Basic
ClassFieldTheory.Mathlib.Algebra.Order.Group.OrderIso
ClassFieldTheory.Mathlib.Algebra.Order.GroupWithZero.Canonical
ClassFieldTheory.Mathlib.Algebra.Order.Hom.Monoid
ClassFieldTheory.Mathlib.Order.Filter.Bases.Monotone
ClassFieldTheory.Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
ClassFieldTheory.Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
ClassFieldTheory.Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
ClassFieldTheory.Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
ClassFieldTheory.Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
ClassFieldTheory.Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
ClassFieldTheory.Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
ClassFieldTheory.Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
ClassFieldTheory.Mathlib.RingTheory.LocalRing.ResidueField.Basic
ClassFieldTheory.Mathlib.RingTheory.Localization.AtPrime.Basic
ClassFieldTheory.Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
ClassFieldTheory.Mathlib.Topology.Algebra.Group.Basic
ClassFieldTheory.Mathlib.Topology.Algebra.IsUniformGroup.Basic
ClassFieldTheory.Mathlib.Topology.Algebra.Module.FiniteDimension
ClassFieldTheory.Mathlib.Topology.Algebra.Ring.Basic
ClassFieldTheory.Mathlib.Topology.Algebra.Valued.NormedValued
ClassFieldTheory.Mathlib.Topology.Algebra.Valued.ValuativeRel
Imported by