leanprover-community/mathlib

Pull Requests Commits

fix(real/sign): make `real.sign 0 = 0` to match `int.sign 0` (#8080)

eric-wieser committed 4 years ago

6666ba2f

docs(data/list/chain): add module docstring (#8041)

YaelDillies committed 4 years ago

a7faaf53

docs(data/list/range): add module docstring (#8026)

YaelDillies committed 4 years ago

cf4a2df2

feat(ring_theory/nilpotent): basic results about nilpotency in associative rings (#8055)

ocfnash committed 4 years ago

9cc44ba2

chore(data/complex/{module, is_R_or_C}, analysis/complex/basic): rationalize the structure provided for `conj` and `of_real` (#8014)

hrmacbeth committed 4 years ago

1774cf95

feat(ring_theory/power_basis): map a power basis through an alg_equiv (#8039)

Vierkantor committed 4 years ago

c5153466

docs(overview, undergrad): add Liouville's Theorem on existence of transcendental numbers (#8068)

adomani committed 4 years ago

10cd252f

feat(data/matrix/basic): add lemma minor_map (#8074)

faenuccio committed 4 years ago

26082445

chore(algebraic_topology/simplex_category): golf proof (#8076)

kbuzzard committed 4 years ago

e137523a

feat(linear_algebra/pi): add linear_equiv.Pi_congr_left (#8070)

eric-wieser committed 4 years ago

e605b21f

chore(field_theory): turn `intermediate_field.subalgebra.equiv_of_eq` into `intermediate_field.equiv_of_eq` (#8069)

Vierkantor committed 4 years ago

25d8aac6

feat(data/polynomial): `aeval_alg_equiv`, like `aeval_alg_hom` (#8038)

Vierkantor committed 4 years ago

db84f2b6

chore(data/polynomial): generalize `aeval_eq_sum_range` to `comm_semiring` (#8037)

Vierkantor committed 4 years ago

2a155208

docs(data/list/pairwise): add module docstring (#8025)

YaelDillies committed 4 years ago

3937c1b2

feat(analysis/convex/exposed): introduce exposed sets (#7928)

YaelDillies committed 4 years ago

520e79d9

feat(measure_theory): the Vitali-Caratheodory theorem (#7766)

sgouezel committed 4 years ago

4801fa66

chore(linear_algebra): switch to named constructors for linear_map (#8059)

eric-wieser committed 4 years ago

b9bf921c

chore(data/polynomial/eval, ring_theory/polynomial_algebra): golfs (#8058)

eric-wieser committed 4 years ago

2a1cabea

feat(data/matrix/basic.lean) : added map_scalar and linear_map.map_matrix (#8061)

faenuccio committed 4 years ago

5352639d

feat(analysis/liouville/liouville_constant): transcendental Liouville numbers exist! (#8020)

adomani committed 4 years ago

5bd649fb

feat(data/nat/prime): norm_num plugin for factors (#8009)

digama0 committed 4 years ago

f7f12bc6

feat(topology/topological_fiber_bundle): a new standard construction for topological fiber bundles (#7935)

Nicknamen committed 4 years ago

d9dcf699

refactor(algebra/ordered_monoid): use `covariant + contravariant` typeclasses in `algebra/ordered_monoid` (#7999)

adomani committed 4 years ago

2f27046f

feat(data/fin): some lemmas about casts (#8049)

ericrbg committed 4 years ago

56535164

chore(data/real/hyperreal): remove @ in a proof (#8063)

adomani committed 4 years ago

e07a24a1

chore(linear_algebra): deduplicate `linear_equiv.{Pi_congr_right,pi}` (#8056)

Vierkantor committed 4 years ago

b9ef710e

feat(measure_theory/set_integral): the set integral is continuous (#7931)

RemyDegenne committed 4 years ago

3cf80395

feat(category_theory/arrow/limit): limit cones in arrow categories (#7457)

jcommelin committed 4 years ago

a31e3c3c

docs(data/fin2): add module docstring (#8047)

YaelDillies committed 4 years ago

204ca5f9

docs(data/option/defs): add module and def docstrings (#8042)

YaelDillies committed 4 years ago

89b8e0b2

Newer Older