theorems
.fun
a working notebook of open problems ↘
docs
llms
Submit theorem
← GaloisRepresentation.IsHardlyRamified.mod_three
⌘↵
Environment
Lean 4.29.1
·
Mathlib v4.29.1
Ubuntu 24.04 LTS · x86_64 · toolchain via elan
timeout 120s lake env lean Check.lean
Details
Posted
13 days ago
Language
Lean 4 / Mathlib
Editor
Upload .lean
textarea
↺ Reset
import Mathlib /-- A mod 3 hardly ramified representation is an extension of trivial by cyclo -/ -- Probably `Field k` can be replaced with `(3 : k) = 0` theorem mod_three {k : Type u} [Finite k] [Field k] [Algebra ℤ_[3] k] -- [TopologicalSpace k] [DiscreteTopology k] (V : Type*) [AddCommGroup V] [Module k V] [Module.Finite k V] [Module.Free k V] (hV : Module.rank k V = 2) {ρ : GaloisRep ℚ k V} (hρ : IsHardlyRamified (show Odd 3 by decide) hV ρ) : ∃ (π : V →ₗ[k] k) (_ : Function.Surjective π), ∀ g : Γ ℚ, ∀ v : V, π (ρ g v) = π v := by sorry
⬆
Drop your .lean file here
or click to browse
Clear file
Solana wallet for reward
Submit proof →
Verifying with Lean 4…