LocalizedModule 📖 | CompOp | 87 mathmath: IsLocalizedModule.iso_symm_apply', Module.Finite.instLocalizationLocalizedModule, LocalizedModule.subsingleton_iff_disjoint, LocalizedModule.smul'_mul, LocalizedModule.restrictScalars_map_eq, Module.Flat.localizedModule, IsLocalizedModule.exists_subsingleton_away, Module.freeLocus_localization, Module.FinitePresentation.exists_notMem_bijective, LocalizedModule.mk_add_mk, IsLocalizedModule.iso_symm_apply, Module.basicOpen_subset_freeLocus_iff, IsLocalizedModule.iso_apply_mk, LocalizedModule.divBy_apply, LocalizedModule.lift'_smul, LocalizedModule.instSubsingleton, LocalizedModule.divBy_mul_by, LocalizedModule.mk_mul_mk, LocalizedModule.map_surjective, IsLocalizedModule.map_surjective_iff_localizedModuleMap_surjective, LocalizedModule.mem_ker_mkLinearMap_iff, IsLocalizedModule.fromLocalizedModule.bij, LocalizedModule.equivTensorProduct_symm_apply_tmul_one, LocalizedModule.equivTensorProduct_apply_mk, LocalizedModule.map_injective, LocalizedModule.equivTensorProduct_symm_apply_tmul, Module.FinitePresentation.linearEquivMap_symm_apply, IsLocalizedModule.iso_symm_comp, IsLocalizedModule.fromLocalizedModule.inj, instSmallLocalizedModule, LocalizedModule.coe_map_eq, LocalizedModule.subsingleton_iff_ker_eq_top, Module.FinitePresentation.exists_free_localizedModule_powers, IsLocalizedModule.fromLocalizedModule_mk, Module.FinitePresentation.linearEquivMap_apply, instFinitePresentationLocalizationLocalizedModule, IsLocalizedModule.lift_comp_iso, LocalizedModule.exists_subsingleton_away, LocalizedModule.smul'_mk, localizedModuleIsLocalizedModule, instIsLocalizedModuleQuotientSubmoduleLocalizedModuleLocalizationLocalizedToLocalizedQuotient, LocalizedModule.mk_neg, LocalizedModule.subsingleton, LocalizedModule.subsingleton_iff, LocalizedModule.smul_def, LocalizedModule.lift_comp, IsLocalizedModule.fromLocalizedModule'_add, Module.FinitePresentation.linearEquivMapExtendScalars_apply, IsLocalizedModule.iso_symm_apply_aux, LocalizedModule.mk_mul_mk', LocalizedModule.lift_mk, Module.FinitePresentation.exists_lift_equiv_of_isLocalizedModule, IsLocalizedModule.map_bijective_iff_localizedModuleMap_bijective, LocalizedModule.mul_by_divBy, LocalizedModule.map_exact, LocalizedModule.subsingleton_iff_support_subset, LocalizedModule.map_id, LocalizedModule.instIsScalarTower, Module.notMem_support_iff, LocalizedModule.algebraMap_mk, LocalizedModule.lift_mk_one, Module.Invertible.instLocalizationLocalizedModule, IsLocalizedModule.mk_eq_mk', IsLocalizedModule.map_injective_iff_localizedModuleMap_injective, LocalizedModule.mk'_smul_mk, Module.mem_support_iff, LocalizedModule.mk_smul_mk, LocalizedModule.smul_eq_iff_of_mem, exists_bijective_map_powers, IsLocalizedModule.iso_localizedModule_eq_refl, LocalizedModule.map_mk, IsLocalizedModule.fromLocalizedModule.surj, LocalizedModule.mul_smul', Module.mem_freeLocus, IsLocalizedModule.map_iso_commute, LocalizedModule.zero_mk, IsLocalizedModule.instIsTorsionFreeLocalizationLocalizedModuleOfIsDomain, LocalizedModule.algebraMap_mk', LocalizedModule.lift'_add, instIsLocalizedModuleLinearMapIdLocalizationLocalizedModuleMapOfFinitePresentation, IsLocalizedModule.map_LocalizedModules, IsLocalizedModule.lift_iso, LocalizedModule.mkLinearMap_apply, Module.FinitePresentation.exists_basis_localizedModule_powers, IsLocalizedModule.fromLocalizedModule'_smul, IsLocalizedModule.iso_mk_one, Module.FinitePresentation.linearEquivMapExtendScalars_symm_apply
|