leanprover-community/mathlib3

Pull Requests Commits

chore(group_theory/exponent): generalise (#13647)

ericrbg committed 3 years ago

1abfde6c

feat(set_theory/game/pgame): Strengthen `move_{left/right}_mk` (#13646)

vihdzp committed 3 years ago

34b1cfd8

fix(topology/algebra/matrix): correct a lemma name (#13640)

eric-wieser committed 3 years ago

44a05db5

feat(data/part): add get_or_else_of_dom (#13588)

BoltonBailey committed 3 years ago

09eb35fd

feat(order/hom/basic): add simp lemmas for `strict_mono.order_iso` and friends (#13606)

ocfnash committed 3 years ago

afd8a525

chore(analysis/normed_space/ray): golf (#13629)

urkud committed 3 years ago

8c262dae

chore(algebra/ring/equiv): protect ring equiv lemmas for big operators (#13624)

j-loreaux committed 3 years ago

4ad7dc9d

feat(algebra/algebra/basic,analysis/normed_space/basic): The zero ring is a (normed) algebra (#13618)

eric-wieser committed 3 years ago

fe435de8

feat(set_theory/pgame): Lemmas about order and left/right moves (#13590)

vihdzp committed 3 years ago

0bea7a08

feat(set_theory/game/pgame): Empty instances (#13635)

vihdzp committed 3 years ago

26b2d727

feat(linear_algebra/basic): add a simp lemma for comp_right (#13625)

antoinelab01 committed 3 years ago

94f970a6

doc(analysis/normed_space/basic): Explain how to use non-unital normed algebras (#13605)

eric-wieser committed 3 years ago

b62b5314

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

leanprover-community-bot committed 3 years ago

79ea30ce

doc(measure_theory): add some missing `to_additive` docstrings (#13456)

urkud committed 3 years ago

9923362c

feat(algebra/order/archimedean): Comparing with rationals determines the order (#13602)

YaelDillies committed 3 years ago

976c544c

feat(topology/uniform_space/matrix): Add the uniform_space structure on matrices (#13534)

eric-wieser committed 3 years ago

b98bd418

chore(*): use zero_lt_two/two_ne_zero lemmas more (#13609)

Ruben-VandeVelde committed 3 years ago

45470769

feat(combinatorics/pigeonhole): Pigeons in linear commutative rings (#13308)

YaelDillies committed 3 years ago

9eb3858a

feat(topology/algebra/group): quotient by a closed subgroup is regular (#13278)

ADedecker committed 3 years ago

7be21e09

feat(order/chain): Flags (#13089)

YaelDillies committed 3 years ago

ad3e6672

feat(data/int/basic): Add unit lemmas (#13565)

tb65536 committed 3 years ago

9c3cb72c

feat(analysis/convex/strict_convex_space): Verify strict convexity from fixed scalars (#13548)

YaelDillies committed 3 years ago

695e0b70

feat(topology/metric_space/hausdorff_distance): Thickening the closure (#13515)

YaelDillies committed 3 years ago

2e83d617

chore(ring_theory/roots_of_unity): primitive roots are not zero (#13587)

ericrbg committed 3 years ago

355d68ab

chore(data/polynomial/degree/definitions): simplify sum_fin, degree_C_le (#13564)

Ruben-VandeVelde committed 3 years ago

79ac4c81

feat(number_theory/legendre_symbol): add file quadratic_char.lean (#13503)

MichaelStollBayreuth committed 3 years ago

a74df9b5

chore(data/rat/basic): tidy some proofs (#13603)

Ruben-VandeVelde committed 3 years ago

631890bf

feat(logic/basic): add `auto_param.out` and `opt_param.out` (#13599)

urkud committed 3 years ago

f7dac5ea

feat(set_theory/game/pgame): simp + private (#13596)

vihdzp committed 3 years ago

6729cca2

refactor(data/nat/factorization): Infer arguments (#13595)

vihdzp committed 3 years ago

62205c27

Newer Older