leanprover-community/mathlib

Pull Requests Commits

vihdzp committed 4 years ago

04b931ab

vihdzp committed 4 years ago

67132f25

Update ordinal_arithmetic.lean

vihdzp committed 4 years ago

282aeaa3

Proved some extra results

vihdzp committed 4 years ago

f40007c6

Started adding a few missing theorems

vihdzp committed 4 years ago

43bafc1a

feat(ring_theory/algebraic): algebraic functions (#11156)

pechersky committed 4 years ago

3f777613

A large amount of progress

vihdzp committed 4 years ago

0a379712

Characterized additive principals

vihdzp committed 4 years ago

ee420686

Merge branch 'lub_new'' into principal

vihdzp committed 4 years ago

15b3b541

vihdzp committed 4 years ago

22cebba2

Started skeleton

vihdzp committed 4 years ago

bcd4d932

Tried fixing breakage again

vihdzp committed 4 years ago

cbcc9c73

Merge branch 'unbounded' into fp_enum_simple

vihdzp committed 4 years ago

da195ace

Added lemmas about bounded intervals

vihdzp committed 4 years ago

7ee1dc9c

Merge branch 'lub_new'' into fp_enum_simple

vihdzp committed 4 years ago

a37c2003

Merge branch 'enum_ord' into fp_enum_simple

vihdzp committed 4 years ago

ec86baf8

Merge branch 'deriv_fp_enum' into fp_enum_simple

vihdzp committed 4 years ago

62dd484a

Merge branch 'unbounded' into deriv_fp_enum

vihdzp committed 4 years ago

9c367cef

Added missing iffs

vihdzp committed 4 years ago

75e2a9a6

vihdzp committed 4 years ago

27371416

feat(topology/algebra/ordered): new lemmas, update (#11184)

urkud committed 4 years ago

ebdbe6b0

chore(measure_theory): fix TC assumptions in 2 lemmas (#11185)

urkud committed 4 years ago

02d02dfc

feat(topology/metric_space/basic): add `fin.dist_insert_nth_insert_nth` (#11183)

urkud committed 4 years ago

c1b10417

chore(order/rel_classes): Removed unnecessary `classical` (#11180)

vihdzp committed 4 years ago

6486e9b3

feat(algebraic_geometry/*): The map `F.stalk y ⟶ F.stalk x` for `x ⤳ y` (#11144)

erdOne committed 4 years ago

93cf56c5

feat(linear_algebra/multilinear/basic): the space of multilinear maps is finite-dimensional when the components are finite-dimensional (#10504)

ocfnash committed 4 years ago

892d465a

feat(combinatorics/configuration): Line count equals point count (#11169)

tb65536 committed 4 years ago

53533697

feat(group_theory/specific_groups/*): computes the exponents of the dihedral and generalised quaternion groups (#11166)

Julian-Kuelshammer committed 4 years ago

a6c82afb

feat(data/nat/log): log_mul, log_div (#11164)

pechersky committed 4 years ago

ad76a5ee

feat(algebraic_geometry): The function field of an integral scheme (#11147)

erdOne committed 4 years ago

23b01cc4

Newer Older