Theorem surjective_fontaineTheta

Modification history

2025-12-11 08:08

Mathlib/RingTheory/Perfectoid/FontaineTheta.lean

feat(RingTheory/Perfectoid): Fontaine's theta map is surjective (#26384) …

Added surjective_fontaineTheta View on Github →