| Name | Category | Theorems |
|---|
constantCoeff 📖 | CompOp | 4 mathmath: constantCoeff_surjective, quotientPEquiv_mk, ker_constantCoeff, constantCoeff_apply
|
ghostComponent 📖 | CompOp | 13 mathmath: ghostComponent_apply, ghostComponent_verschiebungFun, pow_dvd_ghostComponent_of_dvd_coeff, ghostComponent_frobeniusFun, ker_map_le_ker_mk_comp_ghostComponent, ghostMap_apply, ghostComponent_verschiebung, ghostComponent_zero_verschiebung, ghostComponent_frobenius, quotEquivOfEq_ghostComponentModPPow, ghostComponent_zero_verschiebungFun, ghostComponent_teichmuller, ghostComponentModPPow_map_mk
|
ghostEquiv 📖 | CompOp | 1 mathmath: ghostEquiv_coe
|
ghostMap 📖 | CompOp | 3 mathmath: ghostMap.bijective_of_invertible, ghostMap_apply, ghostEquiv_coe
|
instCommRing 📖 | CompOp | 105 mathmath: ghostMap.bijective_of_invertible, map_id, coeff_truncate, toZModPow_compat, constantCoeff_surjective, teichmuller_mul_pow_coeff_of_ne, verschiebung_zmod, truncate_comp_lift, ghostComponent_apply, ghostComponent_verschiebungFun, eq_iterate_verschiebung, IsocrystalHom.frob_equivariant, frobeniusEquiv_symm_apply, TruncatedWittVector.iInf_ker_truncate, factorPowSucc_comp_fontaineThetaModPPow, map_teichmuller, verschiebung_coeff_succ, map_coeff, TruncatedWittVector.truncate_wittVector_truncate, factorPowSucc_fontaineThetaModPPow_eq, teichmuller_zero, iterate_verschiebung_mul, verschiebung_nonzero, frobenius_isPoly, truncate_surjective, mk_pow_fontaineTheta, verschiebung_injective, map_injective, fromPadicInt_comp_toPadicInt, frobenius_bijective, frobenius_frobeniusRotation, instIsDomain, sum_coeff_eq_coeff_sum, mem_span_p_pow_iff_le_coeff_eq_zero, IsocrystalEquiv.frob_equivariant, pow_dvd_ghostComponent_of_dvd_coeff, mem_ker_truncate, fromPadicInt_comp_toPadicInt_ext, TruncatedWittVector.truncate_comp_wittVector_truncate, ghostComponent_frobeniusFun, exists_eq_pow_p_mul', isDiscreteValuationRing, iterate_verschiebung_coeff_eq_zero, dvd_sub_sum_teichmuller_iterateFrobeniusEquiv_coeff, IsPoly.map, ker_map_le_ker_mk_comp_ghostComponent, fontaineThetaModPPow_teichmuller, verschiebung_coeff_zero, iterate_frobenius_coeff, inv_pair₂, irreducible, exists_frobenius_solution_fractionRing, ghostComponentModPPow_teichmuller_coeff, iterate_verschiebung_iterate_frobenius, verschiebung_mul_frobenius, coeff_frobenius_charP, liftEquiv_apply, isAdicCompleteIdealSpanP, ghostMap_apply, inv_pair₁, ghostComponent_verschiebung, surjective_fontaineTheta, map_verschiebung, verschiebung_frobenius, fontaineTheta_teichmuller, truncate_lift, ghostComponent_zero_verschiebung, StandardOneDimIsocrystal.frobenius_apply, iterate_verschiebung_mul_coeff, liftEquiv_symm_apply_coe, quotientPEquiv_mk, toPadicInt_comp_fromPadicInt_ext, map_eq_zero_iff, toPadicInt_comp_fromPadicInt, verschiebung_shift, ghostComponent_frobenius, isUnit_of_coeff_zero_ne_zero, verschiebung_frobenius_comm, quotEquivOfEq_ghostComponentModPPow, teichmuller_coeff_zero, exists_frobenius_solution_fractionRing_aux, iterate_verschiebung_mul_left, iterate_verschiebung_coeff, frobeniusEquiv_apply, truncate_mk', map_surjective, IsPoly₂.map, verschiebung_coeff_add_one, ker_constantCoeff, teichmuller_mul_pow_coeff, aeval_verschiebungPoly, verschiebung_isPoly, constantCoeff_apply, coe_mkUnit, mem_span_p_iff_coeff_zero_eq_zero, ghostEquiv_coe, teichmuller_coeff_pos, mk_fontaineTheta, ghostComponent_zero_verschiebungFun, coeff_frobenius, frobenius_verschiebung, ghostComponent_teichmuller, truncate_liftFun, ghostComponentModPPow_map_mk, frobenius_zmodp
|
map 📖 | CompOp | 13 mathmath: map_id, frobeniusEquiv_symm_apply, map_teichmuller, map_coeff, map_injective, frobenius_eq_map_frobenius, IsPoly.map, ker_map_le_ker_mk_comp_ghostComponent, map_verschiebung, map_eq_zero_iff, map_surjective, IsPoly₂.map, ghostComponentModPPow_map_mk
|
mapFun 📖 | CompOp | 13 mathmath: mapFun.zero, mapFun.surjective, mapFun.nsmul, mapFun.add, mapFun.one, mapFun.sub, mapFun.pow, mapFun.mul, mapFun.zsmul, mapFun.intCast, mapFun.natCast, mapFun.injective, mapFun.neg
|
«tacticGhost_fun_tac_,_» 📖 | CompOp | — |