leanprover-community/mathlib

Pull Requests Commits

rearrange lemma structure

LAC1213 committed 4 years ago

a273625e

strategy for next step

LAC1213 committed 4 years ago

d0a1384c

LAC1213 committed 4 years ago

55ba94d3

feat(ring_theory/discrete_valuation_ring) A local noetherian integral domain of dimension one whose maximal ideal is principal is a discrete valuation ring.

LAC1213 committed 4 years ago

03ddb98a

feat(data/real/ennreal): add `ennreal.prod_lt_top` (#5602)

urkud committed 4 years ago

3669cb35

chore(logic/function): generalize `rel_update_iff` to `forall_update_iff` (#5601)

urkud committed 4 years ago

41501369

fix(data/nat/basic): fix typos in docstrings (#5592)

kbuzzard committed 4 years ago

6acf99e8

feat(data/*, order/*) supporting lemmas for characterising well-founded complete lattices (#5446)

Oliver Nash committed 4 years ago

afbf47d5

chore(scripts): update nolints.txt (#5598)

leanprover-community-bot committed 4 years ago

24340238

doc(overview): add dynamics and `measure.pi` (#5597)

urkud committed 4 years ago

1503cf89

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

Older