Yamaguchi26AbfaithfulGalois.formalHilbert90_galois_of_charP
In characteristic p, every orientation trivial modulo p satisfies formal Hilbert 90 on a separably closed Galois extension.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace Yamaguchi26AbfaithfulGalois
universe u v
variable (p : ℕ) [Fact p.Prime]
variable (K : Type u) (Ω : Type v) [Field K] [Field Ω] [Algebra K Ω]Lean source · statement
theorem formalHilbert90_galois_of_charP
[IsGalois K Ω] [IsSepClosed Ω] [CharP Ω p]
(θ : Orientation p Gal(Ω/K))
(hθ : ∀ g : Gal(Ω/K), PadicInt.toZModPow 1 (θ g : PadicInt p) = 1) :
FormalHilbert90 θ