leanprover-community/mathlib

Pull Requests Commits

chore(algebra/star/self_adjoint): extract a lemma from `has_scalar` (#12121)

eric-wieser committed 4 years ago

223f1496

doc(analysis/normed/group/basic): add docstring explaining the "insert" name (#12100)

eric-wieser committed 4 years ago

aed97e03

fix(category_theory/limits/shapes/images): make class a Prop (#12119)

jcommelin committed 4 years ago

3e6439cd

refactor(topology/algebra): reorder imports (#12089)

urkud committed 4 years ago

33b4e739

feat(data/finset/basic): add lemma `filter_eq_empty_iff` (#12104)

stuart-presnell committed 4 years ago

77f264f1

feat(algebra/indicator_function): smul lemmas for functions (#12059)

sgouezel committed 4 years ago

bb1b56c7

feat(topology/algebra): generalize `has_continuous_smul` arguments to `has_continuous_const_smul` (#11999)

eric-wieser committed 4 years ago

17b3357b

feat(linear_algebra/finite_dimensional): finrank_range_of_inj (#12067)

hparshall committed 4 years ago

b7572061

feat(data/finset/locally_finite): add Ico_subset_Ico_union_Ico (#11710)

BoltonBailey committed 4 years ago

59a183a1

feat(topology/instances/discrete): instances for the discrete topology (#11349)

RemyDegenne committed 4 years ago

e93996cf

feat(data/nat/totient): add Euler's product formula for totient function (#11332)

stuart-presnell committed 4 years ago

6089f08a

feat(analysis/inner_product_space/basic) : `inner_map_self_eq_zero` (#12065)

hparshall committed 4 years ago

19534b29

Revert "feat(category_theory/limits): is_bilimit"

TwoFX committed 4 years ago

8b6901b6

feat(category_theory/limits): is_bilimit

TwoFX committed 4 years ago

8edfa75d

feat(group_theory/commensurable): Definition and lemmas about commensurability. (#9545)

CBirkbeck committed 4 years ago

aacc36c5

feat(category_theory/limits): preservation of zero morphisms (#12068)

TwoFX committed 4 years ago

8575f592

chore(*): update to lean 3.39.2c (#12102)

gebner committed 4 years ago

c9e8c647

feat(order/filter/basic): add eventually_eq.(smul/const_smul/sup/inf) (#12101)

RemyDegenne committed 4 years ago

dcb28262

feat(group_theory/general_commutator): subgroup.pi commutes with the general_commutator (#11825)

nomeata committed 4 years ago

307711e2

feat(data/matrix/notation): expansions of matrix multiplication for 2x2 and 3x3 (#12088)

eric-wieser committed 4 years ago

b54f44f0

fix(topology/algebra/basic): remove duplicate lemma (#12097)

eric-wieser committed 4 years ago

eb8d58d6

feat(measure_theory/integral): add `integral_sum_measure` (#12090)

urkud committed 4 years ago

4afd667f

feat(ring_theory/discriminant): add discr_eq_discr_of_to_matrix_coeff_is_integral (#11994)

riccardobrasca committed 4 years ago

20cf3ca0

feat(order/category/DistribLattice): The category of distributive lattices (#12092)

YaelDillies committed 4 years ago

614758eb

feat(analysis/inner_product_space/pi_L2): `complex.isometry_of_orthonormal` (#11970)

jsm28 committed 4 years ago

58a37203

feat(topology/metric_space/gluing): metric space structure on sigma types (#11965)

sgouezel committed 4 years ago

a355d88c

feat(algebra/group_power/basic): `two_zsmul` (#12094)

jsm28 committed 4 years ago

09960ea1

feat(category_theory/limits): Preserves epi of preserves pushout. (#12084)

erdOne committed 4 years ago

1831d852

chore(algebra/star/self_adjoint): improve definitional unfolding of pow and div (#12085)

eric-wieser committed 4 years ago

84f12be1

feat(topology/continuous_function/algebra): generalize algebra instances (#12055)

eric-wieser committed 4 years ago

834fd30b

Newer Older