leanprover-community/mathlib3

Pull Requests Commits

feat(topology/algebra/floor_ring): add basic topological facts about `floor`, `ceil` and `fract` (#4042)

ADedecker committed 5 years ago

c259305a

feat(logic/basic): apply_dite2, apply_ite2 (#4050)

jsm28 committed 5 years ago

f253fa06

feat(algebraic_geometry/structure_sheaf): stalk_iso (#4047)

kckennylau committed 5 years ago

94b96cff

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

leanprover-community-bot committed 5 years ago

2e198b4a

feat(category_theory): definition of `diag` in `binary_products` (#4051)

cipher1024 committed 5 years ago

4662b203

cleanup(ring_theory/ring_invo): update old module doc, add ring_invo.involution with cleaner statement (#4052)

kim-em committed 5 years ago

4945c778

feat(analysis/normed_space/real_inner_product): linear independence of orthogonal vectors (#4045)

jsm28 committed 5 years ago

de03e191

feat(linear_algebra): Add lemmas about powers of endomorphisms (#4036)

abentkamp committed 5 years ago

1117ae79

feat(analysis/special_functions/trigonometric): Added lemmas for deriv of tan (#3746)

benjamindavidson committed 5 years ago

fabf34f4

feat(data/mv_polynomial): fill in API for vars (#4018)

robertylewis committed 5 years ago

62963861

chore(data/finset/lattice): remove unneeded assumptions (#4020)

jcommelin committed 5 years ago

7b3c653b

feat(computability/encoding): define encoding of basic data types (#3976)

MadPidgeon committed 5 years ago

815a2f97

feat(linear_algebra/char_poly): rephrase Cayley-Hamilton with `aeval', define `matrix.min_poly` (#4040)

awainverse committed 5 years ago

364d5d4c

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

leanprover-community-bot committed 5 years ago

ccd502af

refactor(geometry/manifold): use a sigma type for the total space of the tangent bundle (#3966)

sgouezel committed 5 years ago

7c9a86d4

refactor(field_theory/minimal_polynomial, *): make `aeval`, `is_integral`, and `minimal_polynomial` noncommutative (#4001)

awainverse committed 5 years ago

ecf18c69

doc(slim_check): add suggestion (#4024)

cipher1024 committed 5 years ago

e3057ba4

feat(slim_check): subtype instances for `le` `lt` and `list.perm` (#4027)

cipher1024 committed 5 years ago

a056ccbb

feat(data/padics): universal property of Z_p (#3950)

robertylewis committed 5 years ago

2d40d9c6

ci(scripts/detect_errors.py): enforce silent builds (#4025)

fpvandoorn committed 5 years ago

49173c00

feat(category_theory/filtered): finite diagrams in filtered categories admit cocones (#4026)

kim-em committed 5 years ago

8b277a95

feat(category_theory/limits/concrete): simp lemmas (#3973)

kim-em committed 5 years ago

fa6485a5

feat(geometry/euclidean/circumcenter): more lemmas (#4028)

jsm28 committed 5 years ago

dd633c28

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

leanprover-community-bot committed 5 years ago

c86359f7

fix(docs/100.yaml): fix indentation in 100 list (#4029)

Qian Hong committed 5 years ago

ca5703d5

fix(test/*): make sure tests produce no output (#3947)

fpvandoorn committed 5 years ago

7b9db99c

feat(order/rel_iso): define `rel_hom` (relation-preserving maps) (#3946)

awainverse committed 5 years ago

9d42f6c6

feat(linear_algebra/affine_space): more lemmas (#3990)

jsm28 committed 5 years ago

57463fa4

chore(topology/sheaves): depend less on rfl (#3994)

kim-em committed 5 years ago

71ef45e2

chore(algebra/category/CommRing/limits): don't use deprecated.subring (#4010)

kim-em committed 5 years ago

895f6ee7

Newer Older