leanprover-community/mathlib3

Pull Requests Commits

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

gebner committed 3 years ago

c9e8c647

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

RemyDegenne committed 3 years ago

dcb28262

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

nomeata committed 3 years ago

307711e2

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

eric-wieser committed 3 years ago

b54f44f0

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

eric-wieser committed 3 years ago

eb8d58d6

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

urkud committed 3 years ago

4afd667f

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

riccardobrasca committed 3 years ago

20cf3ca0

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

YaelDillies committed 3 years ago

614758eb

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

jsm28 committed 3 years ago

58a37203

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

sgouezel committed 3 years ago

a355d88c

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

jsm28 committed 3 years ago

09960ea1

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

erdOne committed 3 years ago

1831d852

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

eric-wieser committed 3 years ago

84f12be1

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

eric-wieser committed 3 years ago

834fd30b

feat(topology/instances/rat): some facts about topology on `rat` (#11832)

urkud committed 3 years ago

27df8a0d

feat(topology/metric_space/basic): ext lemmas for metric spaces (#12070)

sgouezel committed 3 years ago

7dae87fe

feat(analysis/specific_limits): useful specializations of some lemmas (#12069)

sgouezel committed 3 years ago

5db1ae4c

feat(data/equiv/{basic,mul_equiv)}: add Pi_subsingleton (#12040)

nomeata committed 3 years ago

1bf41817

feat(field_theory/is_alg_closed): alg closed and char p implies perfect (#12037)

robertylewis committed 3 years ago

b2aaece0

feat(algebra/char_p/basic): add ring_char_of_prime_eq_zero (#12024)

Jlh18 committed 3 years ago

bd67e852

feat(data/part): Instance lemmas (#12001)

BoltonBailey committed 3 years ago

0fe91d0d

chore(data/finsupp/pointwise): golf using injective lemmas (#12086)

eric-wieser committed 3 years ago

b395a671

chore(topology/continuous_function/bounded): golf algebra instances (#12082)

eric-wieser committed 3 years ago

0ab9b5f3

chore(ring_theory/fractional_ideal): golf (#12076)

eric-wieser committed 3 years ago

d86ce027

feat(logic/basic): Better congruence lemmas for `or`, `or_or_or_comm` (#12004)

YaelDillies committed 3 years ago

15c6eee7

feat(category_theory/category/PartialFun): The category of types with partial functions (#11866)

YaelDillies committed 3 years ago

5e3d465c

docs(group_theory/semidirect_product): fix typo in module docs (#12083)

nomeata committed 3 years ago

3c78d00a

feat(algebra/char_p/basic): Generalize `frobenius_inj`. (#12079)

adamtopaz committed 3 years ago

3107a831

feat(data/finset/basic): When `insert` is injective and other lemmas (#11982)

YaelDillies committed 3 years ago

0eb160a5

feat(order/antisymmetrization): Turning a preorder into a partial order (#11728)

YaelDillies committed 3 years ago

6bcb12c1

Newer Older