FLT/GaloisRepresentation/HardlyRamified/Family.lean

GitHub source file

1 declarations, 1 contain sorry, 0 declared as axioms

Hardly ramified representations in compatible families

We show that the property of being hardly ramified is preserved within compatible families of Galois representations.

Imports (2)
Imported by 1 file
  1. theorem GaloisRepresentation.IsHardlyRamified.mem_isCompatible sorry line 37 source

    depends on sorry what this means

    Statement uses: Nat, Odd, Fact, Nat.Prime, CommRing, Algebra, PadicInt, IsDomain, Module.Finite, TopologicalSpace, IsTopologicalRing, IsLocalRing, IsModuleTopology, AddCommGroup, Module, Module.Free, Eq, Cardinal, Module.rank, OfNat.ofNat and 22 more

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    120 instances, coercions and auxiliary constants left out.