Commit 2023-04-12 19:26 7e7ba10b

View on Github →

chore: tidy various files (#3408)

Estimated changes

Modified Mathlib/Algebra/Module/Projective.lean

Modified Mathlib/Analysis/Convex/Function.lean

Modified Mathlib/Analysis/LocallyConvex/Polar.lean

Modified Mathlib/Analysis/Normed/Order/Basic.lean

Modified Mathlib/Analysis/NormedSpace/Basic.lean

added theorem nnnorm_algebraMap'

deleted theorem nnnorm_algebra_map'

added theorem norm_algebraMap'

deleted theorem norm_algebra_map'

Modified Mathlib/CategoryTheory/Idempotents/Karoubi.lean

Modified Mathlib/CategoryTheory/IsConnected.lean

Modified Mathlib/CategoryTheory/Limits/Types.lean

modified def CategoryTheory.Limits.Types.colimitCocone

modified def CategoryTheory.Limits.Types.limitCone

modified def CategoryTheory.Limits.Types.monoFactorisation

Modified Mathlib/CategoryTheory/Preadditive/AdditiveFunctor.lean

Modified Mathlib/Computability/RegularExpressions.lean

Modified Mathlib/Data/Seq/Seq.lean

added theorem Stream'.Seq.get?_nil

added theorem Stream'.Seq.nats_get?

deleted theorem Stream'.Seq.nats_nth

deleted theorem Stream'.Seq.nth_nil

Modified Mathlib/LinearAlgebra/FreeModule/Basic.lean

Modified Mathlib/LinearAlgebra/InvariantBasisNumber.lean

Modified Mathlib/LinearAlgebra/Isomorphisms.lean

Modified Mathlib/RingTheory/EuclideanDomain.lean

Modified Mathlib/RingTheory/FiniteType.lean

Modified Mathlib/RingTheory/Finiteness.lean

modified theorem Subalgebra.fg_bot_toSubmodule

deleted theorem Submodule.fg_bsupr

added theorem Submodule.fg_bsupᵢ

Modified Mathlib/Topology/Category/Top/Basic.lean

Modified Mathlib/Topology/MetricSpace/CauSeqFilter.lean

deleted theorem cau_seq_iff_cauchySeq

added theorem isCauSeq_iff_cauchySeq

Modified Mathlib/Topology/MetricSpace/Contracting.lean

added theorem ContractingWith.efixedPoint_isFixedPt'

deleted theorem ContractingWith.efixedPoint_is_fixed_pt'

Modified Mathlib/Topology/MetricSpace/Gluing.lean