leanprover-community/mathlib

Pull Requests Commits

irreducibility is a lie

b-mehta committed 3 years ago

f2903686

leave with_zero irreducible

YaelDillies committed 3 years ago

aaaa2dfe

YaelDillies committed 3 years ago

5bed0b86

YaelDillies committed 3 years ago

a2017b0f

finish the equivalence

YaelDillies committed 3 years ago

f947dbdd

YaelDillies committed 3 years ago

2491546e

YaelDillies committed 3 years ago

5d8d1308

style(analysis/inner_product_space/l2_space): small style improvement (#15698)

ADedecker committed 3 years ago

10aeb392

feat(set_theory/zfc/basic): `inj` lemmas (#15545)

vihdzp committed 3 years ago

8050ac7c

feat(analysis/inner_product_space): in finite dimension, hilbert basis = orthonormal basis (#15540)

ADedecker committed 3 years ago

c6357eeb

chore(topology/sequences): drop local notation `x ⟶ a` (#15696)

urkud committed 3 years ago

f3e89fb4

chore(data/list/of_fn): injectivity (#15695)

eric-wieser committed 3 years ago

4a6e8cff

feat(analysis/inner_product/pi_L2): a finite orthonormal family is a basis of its span (#15481)

ADedecker committed 3 years ago

fc5a82e1

feat(set/intervals/monotone): add some monotonicity lemmas (#14896)

kex-y committed 3 years ago

eea396ef

chore(data/set/{function,countable}): extract a lemma from a proof (#15668)

urkud committed 3 years ago

fd77cbf2

feat(ring_theory/valuation/valuation_subring): define maximal ideal of valuation subring and provide basic API (#14656)

mckoen committed 3 years ago

8bc2354c

feat(measure_theory/constructions/borel_space): the set of points for which a measurable sequence of functions converges is measurable (#15307)

kex-y committed 3 years ago

70887f86

feat(measure_theory/function/conditional_expectation): pull-out property of the conditional expectation (#15274)

RemyDegenne committed 3 years ago

86f80202

feat(tactic/positivity): a tactic for proving positivity/nonnegativity (#15618)

hrmacbeth committed 3 years ago

e517862a

feat(order/filter/bases): lemmas about bases of product filters (#15630)

urkud committed 3 years ago

8edffc25

chore(number_theory/padics/padic_integers): golf the comm_ring instance (#15590)

eric-wieser committed 3 years ago

671d57dc

feat(probability/moments): mgf/cgf of a sum of independent random variables (#15140)

RemyDegenne committed 3 years ago

e35aa928

feat(category_theory/limits): preserves biproducts if comparison is iso (#14419)

TwoFX committed 3 years ago

c4d273c2

feat(algebraic_topology/fundamental_groupoid): Define simply connected spaces (#12788)

prakol16 committed 3 years ago

38341f11

chore(analysis/inner_product_space): golf two proofs (#15679)

mcdoll committed 3 years ago

b21c9aa1

feat(order/filter/basic): add `filter.has_basis.bInter_mem` (#15661)

urkud committed 3 years ago

8fcb820b

feat(topology/basic): add lemmas about `filter.lift' _ closure` (#15653)

urkud committed 3 years ago

379b72c4

feat(tooplogy/metric_space/hausdorff_distance): add lemmas about `thickening` (#15641)

urkud committed 3 years ago

65d8b84e

chore(topology/locally_finite): move from `topology.basic` (#15640)

urkud committed 3 years ago

b08c7ace

feat(topology/separation): add `disjoint_nhds_nhds` (#15635)

urkud committed 3 years ago

2a9d5695

Older