leanprover-community/mathlib

Pull Requests Commits

vihdzp committed 3 years ago

9a916964

vihdzp committed 3 years ago

87956177

vihdzp committed 3 years ago

c7413170

vihdzp committed 3 years ago

e7496800

vihdzp committed 3 years ago

aae7b869

vihdzp committed 3 years ago

2cc1e97f

I fully expect large amounts of breakage

vihdzp committed 3 years ago

2435ee8e

vihdzp committed 3 years ago

de0e67a2

feat(set_theory/ordinal/basic): Supremum indexed over an empty / unique type (#13735)

vihdzp committed 3 years ago

ce0dc836

chore(logic/relation): Dot notation on `well_founded.trans_gen` (#14016)

vihdzp committed 3 years ago

3a0eb4b5

feat(data/rat/meta_defs, meta/expr): rat.to_pexpr and int.to_pexpr (#14002)

robertylewis committed 3 years ago

e1902256

feat(algebra/{invertible + group_power/lemmas}): taking `inv_of` (⅟_) is injective (#14011)

adomani committed 3 years ago

e0dd3003

chore(order/*): Less `order_dual` abuse (#14008)

YaelDillies committed 3 years ago

0e494afe

chore(order/filter/pointwise): Better definitional unfolding (#13941)

YaelDillies committed 3 years ago

51667657

feat(probability/variance): define the variance of a random variable, prove its basic properties (#13912)

sgouezel committed 3 years ago

cf65daf0

feat(group_theory/group_action/units): simp lemma for scalar action of `is_unit.unit h` (#14006)

sgouezel committed 3 years ago

c2476223

feat(combinatorics/simple_graph/hasse): Hasse diagram and path graph (#13959)

YaelDillies committed 3 years ago

9134a8e7

feat(analysis/calculus/deriv): generalize some lemmas (#13575)

astrainfinita committed 3 years ago

b2aa27e3

feat(algebra/module/linear_map): `Rᵐᵒᵖ` is isomorphic to `module.End R R` (#13931)

haruhisa-enomoto committed 3 years ago

f8bc097d

feat(order/filter): add a few lemmas (#13985)

urkud committed 3 years ago

559f58b1

refactor(algebra/order/monoid_lemmas): reorder the file (#13492)

astrainfinita committed 3 years ago

ca1375a5

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

leanprover-community-bot committed 3 years ago

5789c637

feat(order/atoms): is_atomic_of_order_bot_lt_well_founded (#13967)

kim-em committed 3 years ago

275dabfc

feat(analysis/locally_convex/with_seminorms): characterization of the topology induced by seminorms in terms of `𝓝 0` (#13547)

ADedecker committed 3 years ago

dcd452de

feat(topology/algebra/module/basic): basic topological properties of quotient modules (#13433)

ADedecker committed 3 years ago

10721bab

feat(ring_theory/localization): generalize lemmas from `comm_ring` to `comm_semiring` (#13994)

yuma-mizuno committed 3 years ago

8f116f43

chore(analysis/normed_space/exponential): Make the `𝔸` argument implicit (#13986)

eric-wieser committed 3 years ago

27e105d2

feat(number_theory/legendre_symbol/*): add results on value at -1 (#13978)

MichaelStollBayreuth committed 3 years ago

eea16dc8

feat(data/polynomial/laurent): laurent polynomials -- defs and some API (#13784)

adomani committed 3 years ago

dfe1897f

feat(tactic/lint/misc): adding a linter that flags iffs with explicit variables on both sides (#11606)

arthurpaulino committed 3 years ago

58d83ed5

Older