Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-11 23:40 c0a51cf2

View on Github →

chore(*): update to 3.41.0c (#12591)

Estimated changes

Modified leanpkg.toml

Modified src/algebra/monoid_algebra/to_direct_sum.lean

added def add_monoid_algebra_add_equiv_direct_sum

added def add_monoid_algebra_alg_equiv_direct_sum

added def add_monoid_algebra_ring_equiv_direct_sum

Modified src/analysis/convex/cone.lean

added def set.inner_dual_cone

Modified src/analysis/normed_space/continuous_affine_map.lean

added def continuous_affine_map.to_const_prod_continuous_linear_map

Modified src/analysis/normed_space/linear_isometry.lean

added def linear_isometry_equiv.prod_assoc

Modified src/control/lawful_fix.lean

Modified src/data/complex/is_R_or_C.lean

added def is_R_or_C.conj_ae

added def is_R_or_C.im_lm

added def is_R_or_C.re_lm

Modified src/data/finsupp/to_dfinsupp.lean

added def finsupp_add_equiv_dfinsupp

added def finsupp_lequiv_dfinsupp

Modified src/data/real/ennreal.lean

added def ennreal.of_nnreal_hom

Modified src/measure_theory/constructions/pi.lean

Modified src/measure_theory/measure/haar_lebesgue.lean

added def topological_space.positive_compacts.Icc01

added def topological_space.positive_compacts.pi_Icc01

Modified src/model_theory/direct_limit.lean

added def first_order.language.direct_limit.lift

added def first_order.language.direct_limit.of

Modified src/ring_theory/polynomial/homogeneous.lean

added def mv_polynomial.homogeneous_submodule

Modified src/ring_theory/witt_vector/teichmuller.lean

added def witt_vector.teichmuller

Modified src/tactic/slim_check.lean

Modified src/topology/category/Compactum.lean

added def Compactum_to_CompHaus.iso_of_topological_space