Theorem AdicCompletion.exists_smodEq_pow_smul_top_and_mkQ_eq

Modification history

2025-12-11 08:08
Mathlib/RingTheory/AdicCompletion/Functoriality.lean
feat(RingTheory/Perfectoid): Fontaine's theta map is surjective (#26384) …
Added AdicCompletion.exists_smodEq_pow_smul_top_and_mkQ_eqView on Github →