Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-01-14 08:39
159542ad
View on Github →
chore(*): split some long lines (
#5742
)
Estimated changes
Modified
src/algebra/category/CommRing/basic.lean
modified
def
ring_equiv.to_CommRing_iso
Modified
src/algebra/category/CommRing/limits.lean
Modified
src/algebra/category/Group/zero.lean
Modified
src/algebra/category/Module/basic.lean
modified
def
linear_equiv_iso_Module_iso
Modified
src/algebra/category/Mon/limits.lean
Modified
src/algebra/direct_limit.lean
modified
theorem
add_comm_group.direct_limit.of.zero_exact
modified
theorem
ring.direct_limit.of.zero_exact
Modified
src/algebra/free_algebra.lean
Modified
src/algebra/group/defs.lean
Modified
src/algebra/group_action_hom.lean
modified
theorem
is_invariant_subring.coe_subtype_hom
Modified
src/algebra/group_power/basic.lean
modified
theorem
min_pow_dvd_add
modified
theorem
pow_eq_zero
Modified
src/algebra/invertible.lean
modified
def
invertible.map
modified
theorem
invertible_unique
Modified
src/algebra/lie/basic.lean
modified
theorem
lie_algebra.equiv.coe_to_linear_equiv
modified
theorem
lie_module_equiv.coe_to_lie_module_hom
Modified
src/algebra/lie/classical.lean
Modified
src/algebra/linear_recurrence.lean
Modified
src/algebra/module/basic.lean
Modified
src/algebra/module/ordered.lean
Modified
src/algebra/module/pi.lean
Modified
src/algebra/monoid_algebra.lean
modified
def
add_monoid_algebra.lift_nc_alg_hom
modified
theorem
add_monoid_algebra.lift_nc_one
Modified
src/algebra/ring/pi.lean
Modified
src/algebraic_geometry/Scheme.lean
Modified
src/analysis/analytic/basic.lean
Modified
src/analysis/analytic/composition.lean
modified
theorem
composition.length_sigma_composition_aux
modified
theorem
formal_multilinear_series.comp_coeff_zero''
Modified
src/analysis/calculus/deriv.lean
modified
theorem
has_deriv_within_at.union
Modified
src/analysis/calculus/fderiv.lean
modified
theorem
has_fderiv_within_at.union
Modified
src/analysis/calculus/iterated_deriv.lean
Modified
src/analysis/calculus/mean_value.lean
Modified
src/analysis/hofer.lean
Modified
src/analysis/mean_inequalities.lean
Modified
src/analysis/normed_space/banach.lean
Modified
src/analysis/normed_space/basic.lean
modified
theorem
nnnorm_sum_le
modified
theorem
tsum_of_norm_bounded
Modified
src/analysis/normed_space/inner_product.lean
Modified
src/analysis/normed_space/multilinear.lean
Modified
src/analysis/special_functions/trigonometric.lean
modified
theorem
deriv_within_arctan
modified
theorem
real.angle.sin_eq_iff_eq_or_add_eq_pi
modified
theorem
real.cos_lt_cos_of_nonneg_of_le_pi_div_two
Modified
src/category_theory/adjunction/basic.lean
modified
def
category_theory.adjunction.right_adjoint_of_nat_iso
Modified
src/category_theory/concrete_category/basic.lean
modified
theorem
category_theory.concrete_category.epi_of_surjective
modified
def
category_theory.concrete_category.has_coe_to_sort
modified
theorem
category_theory.concrete_category.mono_of_injective
modified
def
category_theory.forget₂
modified
def
category_theory.has_forget₂.mk'
Modified
src/category_theory/eq_to_hom.lean
modified
theorem
category_theory.eq_to_hom_op
modified
theorem
category_theory.eq_to_hom_unop
Modified
src/category_theory/graded_object.lean
modified
def
category_theory.graded_object_with_shift
Modified
src/combinatorics/pigeonhole.lean
Modified
src/control/uliftable.lean
modified
def
uliftable.down_map
modified
def
uliftable.up_map
Modified
src/data/analysis/filter.lean
modified
theorem
filter.realizer.of_equiv_σ
modified
theorem
filter.realizer.tendsto_iff
Modified
src/data/complex/is_R_or_C.lean
Modified
src/data/equiv/local_equiv.lean
modified
theorem
equiv.refl_to_local_equiv
modified
theorem
local_equiv.of_set_symm
modified
theorem
local_equiv.refl_restr_source
modified
theorem
local_equiv.refl_restr_target
modified
theorem
local_equiv.restr_target
modified
theorem
local_equiv.trans_target
Modified
src/data/fintype/basic.lean
modified
def
fintype.of_surjective
modified
theorem
mem_of_mem_perms_of_list
modified
theorem
mem_perms_of_list_iff
modified
theorem
set.to_finset_inj
Modified
src/data/qpf/multivariate/basic.lean
Modified
src/data/sym.lean
modified
theorem
sym.cons_equiv_eq_equiv_cons
Modified
src/data/typevec.lean
modified
theorem
typevec.const_append1
modified
def
typevec.of_subtype
modified
def
typevec.rel_last'
modified
theorem
typevec.repeat_eq_append1
modified
theorem
typevec.repeat_eq_iff_eq
modified
theorem
typevec.subtype_val_nil
modified
def
typevec.to_subtype
modified
def
typevec.typevec_cases_cons₂
modified
theorem
typevec.typevec_cases_cons₂_append_fun
modified
def
typevec.typevec_cases_nil₃
Modified
src/testing/slim_check/functions.lean
modified
theorem
slim_check.injective_function.apply_id_injective
modified
def
slim_check.injective_function.perm.slice
Modified
src/testing/slim_check/sampleable.lean
modified
def
slim_check.sum.shrink
Modified
src/topology/basic.lean
modified
theorem
interior_union_is_closed_of_interior_empty
Modified
src/topology/metric_space/gromov_hausdorff.lean
modified
theorem
Gromov_Hausdorff.eq_to_GH_space_iff
modified
theorem
Gromov_Hausdorff.to_GH_space_eq_to_GH_space_iff_isometric
Modified
src/topology/metric_space/hausdorff_distance.lean
modified
theorem
emetric.Hausdorff_edist_closure
modified
theorem
emetric.Hausdorff_edist_le_ediam
modified
theorem
emetric.Hausdorff_edist_zero_iff_closure_eq_closure
modified
theorem
emetric.exists_edist_lt_of_Hausdorff_edist_lt
modified
theorem
metric.Hausdorff_dist_closure
Modified
src/topology/metric_space/isometry.lean
modified
theorem
isometry.comp
modified
def
nonempty_compacts.Kuratowski_embedding
Modified
src/topology/separation.lean
modified
theorem
is_compact.finite_compact_cover
modified
theorem
nhds_inter_eq_singleton_of_mem_discrete
Modified
src/topology/sequences.lean
modified
theorem
is_compact.tendsto_subseq'
Modified
src/topology/subset_properties.lean
modified
theorem
is_preconnected_iff_subset_of_disjoint_closed
Modified
src/topology/uniform_space/completion.lean
Modified
src/topology/uniform_space/separation.lean
modified
theorem
eq_of_uniformity_inf_nhds
modified
theorem
separation_rel_comap