leanprover-community/mathlib3

Pull Requests Commits

fix(tactic/rcases): fix rcases? goal alignment (#5576)

digama0 committed 4 years ago

4fcf65c0

feat(measure_theory): almost everywhere measurable functions (#5568)

sgouezel committed 4 years ago

96948e45

feat(data/option/basic): join and associated lemmas (#5426)

pechersky committed 4 years ago

2967793e

feat(measure_theory/interval_integral): FTC-2 (#4945)

benjamindavidson committed 4 years ago

d04e034a

fix(algebra/module/basic): Do not attach the ℕ and ℤ `is_scalar_tower` and `smul_comm_class` instances to a specific definition of smul (#5509)

eric-wieser committed 4 years ago

46c35cc1

feat(measure_theory/lp_space): snorm is zero iff the function is zero ae (#5595)

RemyDegenne committed 4 years ago

e1138b00

feat(measure_theory/lp_space): add triangle inequality for the Lp seminorm (#5594)

RemyDegenne committed 4 years ago

ae2c8572

feat(computability/*FA): Deterministic and Nondeterministic Finite Automata (#5038)

foxthomson committed 4 years ago

384ba88b

feat(analysis/normed_space/basic): basic facts about the sphere (#5590)

hrmacbeth committed 4 years ago

eb6d5f15

feat(measure_theory/pi): finite products of measures (#5414)

fpvandoorn committed 4 years ago

0837fc30

feat(data/equiv/basic): rfl lemma for equiv_congr (#5585)

pechersky committed 4 years ago

e3501142

feat(combinatorics/simple_graph): finitely many simple graphs on a finite type (#5584)

b-mehta committed 4 years ago

57c6d191

feat(data/finset/basic): add `finset.piecewise_le_piecewise` (#5572)

urkud committed 4 years ago

9fc7aa56

chore(data/prod): add `prod.forall'` and `prod.exists'` (#5570)

urkud committed 4 years ago

0a4fbd8c

feat(data/nat/fib): fib n is a strong divisibility sequence (#5555)

Hanting Zhang committed 4 years ago

0dc7a27c

chore(data/finset/sort): upgrade `finset.mono_of_fin` to an `order_iso` (#5495)

urkud committed 4 years ago

9f252442

feat(linear_algebra/alternating): Show the link to linear_independent (#5477)

eric-wieser committed 4 years ago

9ea7e462

feat(group_theory/dihedral): add dihedral groups (#5171)

shingtaklam1324 committed 4 years ago

04f8fd74

doc(overview): pluralization convention (#5583)

kmill committed 4 years ago

ee2c963e

doc(overview): Add alternating_map (#5582)

eric-wieser committed 4 years ago

e6982901

doc(overview): combinatorics section (#5581)

kmill committed 4 years ago

1a39825b

doc(overview): add missing algebras to overview (#5579)

eric-wieser committed 4 years ago

5bff8872

chore(topology/algebra/ordered,analysis/specific_limits): two more limits (#5573)

urkud committed 4 years ago

e0946065

feat(measure_theory/borel_space): the inverse of a closed embedding is measurable (#5567)

sgouezel committed 4 years ago

aa88bb81

chore(number_theory/bernoulli): refactor definition of bernoulli (#5534)

kbuzzard committed 4 years ago

a7d05c45

feat(data/polynomial/erase_lead): add lemma erase_lead_card_support_eq (#5529)

adomani committed 4 years ago

12b5024b

chore(algebra/group,algebra/group_with_zero): a few more injective/surjective constructors (#5547)

urkud committed 4 years ago

fceb7c1a

feat(algebra/group/prod) Units of a product monoid (#5563)

alexjbest committed 4 years ago

e142c825

feat(algebra/ordered_{group,field}): more lemmas relating inv and mul inequalities (#5561)

bryangingechen committed 4 years ago

e35a703f

feat(linear_algebra/dimension): linear equiv iff eq dim (#5559)

adamtopaz committed 4 years ago

f5f879e2

Newer Older