Commit 2023-04-05 08:13 fd515548

View on Github →

feat: port Topology.Instances.TrivSqZeroExt (#3275)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Algebra/ConstMulAction.lean

Modified Mathlib/Topology/Algebra/Group/Basic.lean

Modified Mathlib/Topology/Algebra/Monoid.lean

Modified Mathlib/Topology/Algebra/MulAction.lean

Created Mathlib/Topology/Instances/TrivSqZeroExt.lean

added theorem TrivSqZeroExt.continuous_inl

added theorem TrivSqZeroExt.continuous_inr

added theorem TrivSqZeroExt.embedding_inl

added theorem TrivSqZeroExt.embedding_inr

added def TrivSqZeroExt.fstClm

added theorem TrivSqZeroExt.hasSum_fst

added theorem TrivSqZeroExt.hasSum_inl

added theorem TrivSqZeroExt.hasSum_inr

added theorem TrivSqZeroExt.hasSum_snd

added def TrivSqZeroExt.inlClm

added def TrivSqZeroExt.inrClm

added theorem TrivSqZeroExt.nhds_def

added theorem TrivSqZeroExt.nhds_inl

added theorem TrivSqZeroExt.nhds_inr

added def TrivSqZeroExt.sndClm

added theorem TrivSqZeroExt.topologicalSemiring

Modified Mathlib/Topology/Separation.lean