Commit 2023-04-04 14:45 2dd4be19

View on Github →

feat: port Topology.Algebra.Module.Basic (#2983)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Algebra/ConstMulAction.lean

added theorem isClosed_setOf_map_smul

Created Mathlib/Topology/Algebra/Module/Basic.lean

added def ContinuousLinearEquiv.Simps.apply

added def ContinuousLinearEquiv.Simps.symm_apply

added theorem ContinuousLinearEquiv.apply_symm_apply

added def ContinuousLinearEquiv.arrowCongrEquiv

added theorem ContinuousLinearEquiv.coe_apply

added theorem ContinuousLinearEquiv.coe_coe

added theorem ContinuousLinearEquiv.coe_comp_coe_symm

added theorem ContinuousLinearEquiv.coe_funUnique

added theorem ContinuousLinearEquiv.coe_funUnique_symm

added theorem ContinuousLinearEquiv.coe_inj

added theorem ContinuousLinearEquiv.coe_injective

added theorem ContinuousLinearEquiv.coe_prod

added theorem ContinuousLinearEquiv.coe_refl'

added theorem ContinuousLinearEquiv.coe_refl

added theorem ContinuousLinearEquiv.coe_symm_comp_coe

added theorem ContinuousLinearEquiv.coe_toHomeomorph

added theorem ContinuousLinearEquiv.coe_toLinearEquiv

added theorem ContinuousLinearEquiv.comp_coe

added theorem ContinuousLinearEquiv.comp_continuousOn_iff

added theorem ContinuousLinearEquiv.comp_continuous_iff

added theorem ContinuousLinearEquiv.eq_symm_apply

added def ContinuousLinearEquiv.equivOfInverse

added theorem ContinuousLinearEquiv.equivOfInverse_apply

added def ContinuousLinearEquiv.equivOfRightInverse

added theorem ContinuousLinearEquiv.equivOfRightInverse_symm_apply

added theorem ContinuousLinearEquiv.ext

added theorem ContinuousLinearEquiv.ext₁

added def ContinuousLinearEquiv.finTwoArrow

added theorem ContinuousLinearEquiv.fst_equivOfRightInverse

added def ContinuousLinearEquiv.funUnique

added theorem ContinuousLinearEquiv.image_closure

added theorem ContinuousLinearEquiv.image_symm_image

added theorem ContinuousLinearEquiv.isClosed_image

added theorem ContinuousLinearEquiv.map_add

added theorem ContinuousLinearEquiv.map_eq_zero_iff

added theorem ContinuousLinearEquiv.map_neg

added theorem ContinuousLinearEquiv.map_nhds_eq

added theorem ContinuousLinearEquiv.map_smul

added theorem ContinuousLinearEquiv.map_smulₛₗ

added theorem ContinuousLinearEquiv.map_sub

added theorem ContinuousLinearEquiv.map_zero

added def ContinuousLinearEquiv.ofUnit

added def ContinuousLinearEquiv.piFinTwo

added theorem ContinuousLinearEquiv.preimage_closure

added def ContinuousLinearEquiv.prod

added theorem ContinuousLinearEquiv.prod_apply

added theorem ContinuousLinearEquiv.prod_symm

added theorem ContinuousLinearEquiv.refl_symm

added theorem ContinuousLinearEquiv.self_comp_symm

added def ContinuousLinearEquiv.skewProd

added theorem ContinuousLinearEquiv.skewProd_apply

added theorem ContinuousLinearEquiv.skewProd_symm_apply

added theorem ContinuousLinearEquiv.snd_equivOfRightInverse

added theorem ContinuousLinearEquiv.symm_apply_apply

added theorem ContinuousLinearEquiv.symm_apply_eq

added theorem ContinuousLinearEquiv.symm_comp_self

added theorem ContinuousLinearEquiv.symm_equivOfInverse

added theorem ContinuousLinearEquiv.symm_image_image

added theorem ContinuousLinearEquiv.symm_map_nhds_eq

added theorem ContinuousLinearEquiv.symm_symm

added theorem ContinuousLinearEquiv.symm_symm_apply

added theorem ContinuousLinearEquiv.symm_toHomeomorph

added theorem ContinuousLinearEquiv.symm_toLinearEquiv

added theorem ContinuousLinearEquiv.symm_trans_apply

added def ContinuousLinearEquiv.toContinuousLinearMap

added def ContinuousLinearEquiv.toHomeomorph

added theorem ContinuousLinearEquiv.toLinearEquiv_injective

added def ContinuousLinearEquiv.toUnit

added theorem ContinuousLinearEquiv.trans_apply

added theorem ContinuousLinearEquiv.trans_toLinearEquiv

added def ContinuousLinearEquiv.ulift

added def ContinuousLinearEquiv.unitsEquiv

added def ContinuousLinearEquiv.unitsEquivAut

added theorem ContinuousLinearEquiv.unitsEquivAut_apply

added theorem ContinuousLinearEquiv.unitsEquivAut_apply_symm

added theorem ContinuousLinearEquiv.unitsEquivAut_symm_apply

added theorem ContinuousLinearEquiv.unitsEquiv_apply

added structure ContinuousLinearEquiv

added def ContinuousLinearMap.Simps.apply

added def ContinuousLinearMap.Simps.coe

added theorem ContinuousLinearMap.add_apply

added theorem ContinuousLinearMap.add_comp

added theorem ContinuousLinearMap.closedComplemented_ker_of_rightInverse

added def ContinuousLinearMap.codRestrict

added theorem ContinuousLinearMap.coeFn_injective

added def ContinuousLinearMap.coeLM

added def ContinuousLinearMap.coeLMₛₗ

added theorem ContinuousLinearMap.coe_add'

added theorem ContinuousLinearMap.coe_add

added theorem ContinuousLinearMap.coe_codRestrict

added theorem ContinuousLinearMap.coe_codRestrict_apply

added theorem ContinuousLinearMap.coe_coe

added theorem ContinuousLinearMap.coe_comp'

added theorem ContinuousLinearMap.coe_comp

added theorem ContinuousLinearMap.coe_coprod

added theorem ContinuousLinearMap.coe_copy

added theorem ContinuousLinearMap.coe_eq_id

added theorem ContinuousLinearMap.coe_fst'

added theorem ContinuousLinearMap.coe_fst

added theorem ContinuousLinearMap.coe_id'

added theorem ContinuousLinearMap.coe_id

added theorem ContinuousLinearMap.coe_inj

added theorem ContinuousLinearMap.coe_injective

added theorem ContinuousLinearMap.coe_inl

added theorem ContinuousLinearMap.coe_inr

added theorem ContinuousLinearMap.coe_mk'

added theorem ContinuousLinearMap.coe_mk

added theorem ContinuousLinearMap.coe_mul

added theorem ContinuousLinearMap.coe_neg'

added theorem ContinuousLinearMap.coe_neg

added theorem ContinuousLinearMap.coe_pi'

added theorem ContinuousLinearMap.coe_pi

added theorem ContinuousLinearMap.coe_prod

added theorem ContinuousLinearMap.coe_prodMap

added theorem ContinuousLinearMap.coe_prod_map

added theorem ContinuousLinearMap.coe_projKerOfRightInverse_apply

added theorem ContinuousLinearMap.coe_restrictScalars'

added theorem ContinuousLinearMap.coe_restrictScalars

added theorem ContinuousLinearMap.coe_restrictScalarsₗ

added theorem ContinuousLinearMap.coe_smul'

added theorem ContinuousLinearMap.coe_smul

added theorem ContinuousLinearMap.coe_smulRightₗ

added theorem ContinuousLinearMap.coe_snd'

added theorem ContinuousLinearMap.coe_snd

added theorem ContinuousLinearMap.coe_sub'

added theorem ContinuousLinearMap.coe_sub

added theorem ContinuousLinearMap.coe_sum'

added theorem ContinuousLinearMap.coe_sum

added theorem ContinuousLinearMap.coe_zero'

added theorem ContinuousLinearMap.coe_zero

added def ContinuousLinearMap.comp

added theorem ContinuousLinearMap.comp_add

added theorem ContinuousLinearMap.comp_apply

added theorem ContinuousLinearMap.comp_assoc

added theorem ContinuousLinearMap.comp_id

added theorem ContinuousLinearMap.comp_neg

added theorem ContinuousLinearMap.comp_smul

added theorem ContinuousLinearMap.comp_smulₛₗ

added theorem ContinuousLinearMap.comp_sub

added theorem ContinuousLinearMap.comp_zero

added def ContinuousLinearMap.coprod

added theorem ContinuousLinearMap.coprod_apply

added theorem ContinuousLinearMap.copy_eq

added theorem ContinuousLinearMap.default_def

added theorem ContinuousLinearMap.eqOn_closure_span

added theorem ContinuousLinearMap.exists_ne_zero

added theorem ContinuousLinearMap.ext

added theorem ContinuousLinearMap.ext_iff

added theorem ContinuousLinearMap.ext_on

added theorem ContinuousLinearMap.ext_ring

added theorem ContinuousLinearMap.ext_ring_iff

added def ContinuousLinearMap.fst

added theorem ContinuousLinearMap.fst_comp_prod

added theorem ContinuousLinearMap.fst_prod_snd

added def ContinuousLinearMap.id

added theorem ContinuousLinearMap.id_apply

added theorem ContinuousLinearMap.id_comp

added def ContinuousLinearMap.infᵢKerProjEquiv

added theorem ContinuousLinearMap.infᵢ_ker_proj

added def ContinuousLinearMap.inl

added theorem ContinuousLinearMap.inl_apply

added def ContinuousLinearMap.inr

added theorem ContinuousLinearMap.inr_apply

added theorem ContinuousLinearMap.inverse_equiv

added theorem ContinuousLinearMap.inverse_non_equiv

added theorem ContinuousLinearMap.isClosed_ker

added theorem ContinuousLinearMap.isComplete_ker

added theorem ContinuousLinearMap.ker_codRestrict

added theorem ContinuousLinearMap.ker_coprod_of_disjoint_range

added theorem ContinuousLinearMap.ker_prod

added theorem ContinuousLinearMap.ker_prod_ker_le_ker_coprod

added theorem ContinuousLinearMap.map_smul_of_tower

added theorem ContinuousLinearMap.mul_apply

added theorem ContinuousLinearMap.mul_def

added theorem ContinuousLinearMap.neg_apply

added theorem ContinuousLinearMap.neg_comp

added theorem ContinuousLinearMap.one_apply

added theorem ContinuousLinearMap.one_def

added def ContinuousLinearMap.pi

added theorem ContinuousLinearMap.pi_apply

added theorem ContinuousLinearMap.pi_comp

added theorem ContinuousLinearMap.pi_eq_zero

added theorem ContinuousLinearMap.pi_zero

added def ContinuousLinearMap.prodEquiv

added def ContinuousLinearMap.prodMap

added theorem ContinuousLinearMap.prod_apply

added theorem ContinuousLinearMap.prod_ext

added theorem ContinuousLinearMap.prod_ext_iff

added def ContinuousLinearMap.prodₗ

added def ContinuousLinearMap.proj

added def ContinuousLinearMap.projKerOfRightInverse

added theorem ContinuousLinearMap.projKerOfRightInverse_apply_idem

added theorem ContinuousLinearMap.projKerOfRightInverse_comp_inv

added theorem ContinuousLinearMap.proj_apply

added theorem ContinuousLinearMap.proj_pi

added theorem ContinuousLinearMap.range_coprod

added theorem ContinuousLinearMap.range_prod_eq

added def ContinuousLinearMap.restrictScalars

added theorem ContinuousLinearMap.restrictScalars_add

added theorem ContinuousLinearMap.restrictScalars_neg

added theorem ContinuousLinearMap.restrictScalars_smul

added theorem ContinuousLinearMap.restrictScalars_zero

added def ContinuousLinearMap.restrictScalarsₗ

added theorem ContinuousLinearMap.ring_inverse_eq_map_inverse

added theorem ContinuousLinearMap.ring_inverse_equiv

added def ContinuousLinearMap.smulRight

added theorem ContinuousLinearMap.smulRight_apply

added theorem ContinuousLinearMap.smulRight_comp

added theorem ContinuousLinearMap.smulRight_one_eq_iff

added theorem ContinuousLinearMap.smulRight_one_one

added theorem ContinuousLinearMap.smulRight_one_pow

added def ContinuousLinearMap.smulRightₗ

added theorem ContinuousLinearMap.smul_apply

added theorem ContinuousLinearMap.smul_comp

added def ContinuousLinearMap.snd

added theorem ContinuousLinearMap.snd_comp_prod

added theorem ContinuousLinearMap.sub_apply'

added theorem ContinuousLinearMap.sub_apply

added theorem ContinuousLinearMap.sub_comp

added theorem ContinuousLinearMap.sum_apply

added def ContinuousLinearMap.toLinearMapRingHom

added theorem ContinuousLinearMap.to_ring_inverse

added theorem ContinuousLinearMap.zero_apply

added theorem ContinuousLinearMap.zero_comp

added structure ContinuousLinearMap

added theorem ContinuousSMul.of_nhds_zero

added theorem DenseRange.topologicalClosure_map_submodule

added theorem IsClosed.submodule_topologicalClosure_eq

added theorem LinearMap.continuous_on_pi

added theorem LinearMap.isClosed_range_coe

added theorem Module.punctured_nhds_neBot

added theorem Submodule.ClosedComplemented.has_closed_complement

added def Submodule.ClosedComplemented

added theorem Submodule.closedComplemented_bot

added theorem Submodule.closedComplemented_top

added theorem Submodule.coe_subtypeL'

added theorem Submodule.coe_subtypeL

added theorem Submodule.dense_iff_topologicalClosure_eq_top

added theorem Submodule.eq_top_of_nonempty_interior'

added theorem Submodule.isClosed_or_dense_of_isCoatom

added theorem Submodule.isClosed_topologicalClosure

added theorem Submodule.isOpenMap_mkQ

added theorem Submodule.ker_subtypeL

added theorem Submodule.le_topologicalClosure

added theorem Submodule.mapsTo_smul_closure

added theorem Submodule.range_subtypeL

added theorem Submodule.smul_closure_subset

added def Submodule.subtypeL

added theorem Submodule.subtypeL_apply

added def Submodule.topologicalClosure

added theorem Submodule.topologicalClosure_coe

added theorem Submodule.topologicalClosure_map

added theorem Submodule.topologicalClosure_minimal

added theorem Submodule.topologicalClosure_mono

added theorem continuousSMul_induced

added def linearMapOfMemClosureRangeCoe

added def linearMapOfTendsto