leanprover-community/mathlib3

Pull Requests Commits

YaelDillies committed 3 years ago

3dfaa905

chore(set_theory/game/pgame): minor golf (#14171)

vihdzp committed 3 years ago

df64e5e5

chore(group_theory/specific_groups/cyclic): golf `card_order_of_eq_totient_aux₁` and `card_order_of_eq_totient_aux₂` (#14161)

stuart-presnell committed 3 years ago

f4c67ee5

feat(data/int/basic): add theorem `int.div_mod_unique` (#14158)

Faris999 committed 3 years ago

a5975e73

chore(ring_theory/ideal/local_ring): golf some proofs, add missing lemma (#14157)

Ruben-VandeVelde committed 3 years ago

f7a7c272

feat(data/zmod/quotient): `orbit (zpowers a) b` is a cycle of order `minimal_period ((•) a) b` (#14124)

tb65536 committed 3 years ago

55b31e05

feat(*): Pointwise monoids have distributive negations (#14114)

YaelDillies committed 3 years ago

bc7a201e

feat(algebra/module): morphism classes for (semi)linear maps (#13939)

Vierkantor committed 3 years ago

f0db51d4

doc(set_theory/surreal/basic): update docs (#14170)

vihdzp committed 3 years ago

0d762850

feat(order/cover): Covering elements are unique (#14156)

YaelDillies committed 3 years ago

4cf20164

feat (group_theory/perm/cycles): Add missing `is_cycle` lemma (#13219)

MantasBaksys committed 3 years ago

00e80a63

chore(logic/equiv): golf equiv.subtype_equiv (#14125)

ericrbg committed 3 years ago

c1091050

feat(linear_algebra/matrix): invariant basis number for matrices (#13845)

kim-em committed 3 years ago

843240b0

move(data/prod/*): A `prod` folder (#13771)

YaelDillies committed 3 years ago

f9f64f37

chore(order/lattice): reflow, golf (#14151)

urkud committed 3 years ago

a74298d8

chore(order/conditionally_complete_lattice): General cleanup (#13319)

vihdzp committed 3 years ago

5c954e12

refactor(set_theory/game/*): Fix bad notation `<` on (pre-)games (#13963)

vihdzp committed 3 years ago

b8d8a5e4

feat(linear_algebra/projection) : projections are conjugate to prod_map id 0 (#13802)

antoinelab01 committed 3 years ago

1f00800d

feat(analysis/special_functions/exp_deriv): generalize some lemmas about `complex.exp`, remove `*.cexp_real` (#13579)

astrainfinita committed 3 years ago

e7386121

feat(category_theory): missing comp_ite lemma (#14143)

kim-em committed 3 years ago

570db888

feat(algebra/big_operators): prod_ite_irrel (#14142)

kim-em committed 3 years ago

ad5edeb5

chore(set_theory/ordinal/{basic, arithmetic}): Remove redundant `function` namespace (#14133)

vihdzp committed 3 years ago

05997bda

doc(data/real/sqrt): Fix typo in described theorem (#14126)

timotree3 committed 3 years ago

9d022d77

chore(category_theory/*): move some elementwise lemmas earlier (#13998)

kim-em committed 3 years ago

4125b9ad

feat(set_theory/cardinal/cofinality): Cofinality of `nfp` and `deriv` (#12556)

vihdzp committed 3 years ago

c992b04d

feat(analysis/specific_limits/floor_pow): auxiliary results on series involving floors of powers (#13850)

sgouezel committed 3 years ago

6d4c2027

chore(algebra/invertible): minor golf (#14141)

vihdzp committed 3 years ago

ba9d551a

feat(linear_algebra/matrix/to_lin): equivalence via right multiplication (#13870)

kim-em committed 3 years ago

79bc06bf

chore(*): use notation instead of `set.*` (#14139)

urkud committed 3 years ago

21a71de1

refactor(group_theory/free_abelian_group): Make proofs more robust (#14089)

YaelDillies committed 3 years ago

38244939

Older