leanprover-community/mathlib

Pull Requests Commits

adomani committed 3 years ago

10e93c4d

more attributes

adomani committed 3 years ago

01b055ec

adomani committed 3 years ago

90b71bc6

adomani committed 3 years ago

c0e4f28d

adomani committed 3 years ago

38876c0d

adomani committed 3 years ago

2c5a38c4

adomani committed 3 years ago

271fb9b7

sime simv to simp

adomani committed 3 years ago

783177ac

adomani committed 3 years ago

804dc0f6

move simp -> simv

adomani committed 3 years ago

15f24b66

adomani committed 3 years ago

848753cb

feat(geometry/euclidean/oriented_angle): relation to unoriented angles (#15722)

jsm28 committed 3 years ago

674505ed

feat(algebra/order/floor): `fract_one` (#15785)

jsm28 committed 3 years ago

7dcf5c3d

chore(data/zmod): make `zmod.int_cast_zmod_cast` `@[norm_cast]` (#15753)

Vierkantor committed 3 years ago

2f1b3131

feat(topology/homeomorph): Product of sets is isomorphic to product of sets (#15664)

tb65536 committed 3 years ago

1b09efe3

fix(data/polynomial/basic): remove `monomial_fun` to remove diamonds (#15778)

ericrbg committed 3 years ago

7ad184e3

feat(order/succ_pred/basic): `a ≤ succ ⊥ ↔ a = ⊥ ∨ a = succ ⊥` and related (#15567)

vihdzp committed 3 years ago

9bb1256d

chore(ring_theory/adjoin_root): remove duplicate namespace (#15775)

ericrbg committed 3 years ago

b6fa37ed

feat(probability/density): probability of event in uniform distribution (#15678)

b-mehta committed 3 years ago

9c473c1d

feat(data/nat/factorization/basic): add lemma `prime.factorization_self` (#15767)

stuart-presnell committed 3 years ago

a2a02a30

feat(number_theory): Bertrand's postulate, slightly different approach (#8002)

BoltonBailey committed 3 years ago

7b2ae37e

feat(ring_theory/ideal/operations): A variant of `finsupp.total` for ideals. (#15460)

erdOne committed 3 years ago

5e07117c

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

leanprover-community-bot committed 3 years ago

bff2f20c

chore(logic/function/basic): make `function.injective.decidable_eq` protected (#15759)

ADedecker committed 3 years ago

a574fbe6

feat(algebra/algebra/subalgebra/basic): Swap arguments of `map` and `comap` (#15744)

tb65536 committed 3 years ago

348a674b

refactor(tactic/lint/type_classes): change inhabited linter to nonempty linter (#15542)

kmill committed 3 years ago

14b69e9f

feat(algebra/big_operators): add lemmas about sum of disjoint multiset (#15556)

xroblot committed 3 years ago

20f97964

feat(group_theory/p_group): Groups of order p^2 are commutative (#8632)

ChrisHughes24 committed 3 years ago

09afe572

refactor(algebra/homology): better defeqs, less case splitting (#15690)

jcommelin committed 3 years ago

13ff898b

fix(linear_algebra/prod): add missing `of_dual`s in lemma statements (#15750)

eric-wieser committed 3 years ago

cb3c2b9e

Older