leanprover-community/mathlib3

Pull Requests Commits

feat(data/{int, nat, rat}/cast): extensionality lemmas (#6788)

thejohncrafter committed 4 years ago

272e2d22

feat(topology/algebra/ordered): IVT for the unordered interval (#7237)

benjamindavidson committed 4 years ago

43f63d99

feat(tactic/simps): use new options in library (#7095)

fpvandoorn committed 4 years ago

5993b90e

chore(data/set/basic): add `set.subsingleton.pairwise_on` (#7257)

urkud committed 4 years ago

dbc6574c

feat(data/nat/parity): update to match int/parity (#7156)

benjamindavidson committed 4 years ago

f6132e4d

feat(data/int/parity): update to match nat/parity (where applicable) (#7155)

benjamindavidson committed 4 years ago

969c6a3e

feat(group_theory/submonoid/operations): add lemmas (#7219)

riccardobrasca committed 4 years ago

30ee691e

feat(data/complex): numerical bounds on log 2 (#7146)

b-mehta committed 4 years ago

d107d825

feat(topology/continuous_function): on a subsingleton X, there is only one subalgebra R C(X,R) (#7247)

kim-em committed 4 years ago

7f541b4e

feat(data/finset/lattice): mem_sup, mem_sup' (#7245)

kim-em committed 4 years ago

cab0481e

feat(set_theory/surreal): add add_monoid instance (#7228)

apurvnakade committed 4 years ago

3953378b

feat(topology/algebra/mul_action.lean): add smul_const (#7242)

YaelDillies committed 4 years ago

a6f62a74

chore(data/set/finite): rename some lemmas (#7241)

urkud committed 4 years ago

4d4b501e

feat(algebra/lie/basic): define the `module` and `lie_module` structures on morphisms of Lie modules (#7225)

ocfnash committed 4 years ago

043d046a

feat(data/real): Inf is nonneg (#7223)

b-mehta committed 4 years ago

aa44de5b

feat(linear_algebra): maximal linear independent (#7160)

PatrickMassot committed 4 years ago

c68e718a

chore(.github/workflows/build.yml): update elan script URL (#7234)

bryangingechen committed 4 years ago

ce667c41

refactor(topology/algebra/module): `map_smul` argument swap (#7233)

YaelDillies committed 4 years ago

20db2fb2

feat(analysis/convex/basic): convex hull and empty set (#7232)

b-mehta committed 4 years ago

b2e7f40f

doc(group_theory): fix `normalizer` docstring (#7231)

mguaypaq committed 4 years ago

22924634

feat(data/equiv/mul_add): use `@[simps]` (#7213)

fpvandoorn committed 4 years ago

21d74c7a

feat(data/nat/choose/sum): Add lower bound lemma for central binomial coefficient (#7214)

BoltonBailey committed 4 years ago

9363a649

feat(analysis/normed_space/operator_norm): generalize to seminormed space (#7202)

riccardobrasca committed 4 years ago

e9a11f6e

chore(category_theory/subobject): different proof of le_of_comm (#7229)

TwoFX committed 4 years ago

206ecce7

feat(order/conditionally_complete_lattice): conditional Inf of intervals (#7226)

b-mehta committed 4 years ago

0f6c1f19

feat(category_theory): formally adjoined initial objects are strict (#7222)

TwoFX committed 4 years ago

560a0092

chore(ring_theory/adjoin.basic): use submodule.closure in algebra.adjoin_eq_span (#7194)

riccardobrasca committed 4 years ago

89c16a79

feat(test/integration): improve an example (#7169)

benjamindavidson committed 4 years ago

b7a3d4e1

feat(category_theory/triangulated/pretriangulated): add definition of pretriangulated categories and triangulated functors between them (#7153)

l-kershaw committed 4 years ago

6b182fcd

feat(data/list/basic): fold[rl] recursion principles (#7079)

pechersky committed 4 years ago

110541dd

Newer Older