leanprover-community/mathlib3

Pull Requests Commits

b-mehta committed 3 years ago

3ced9150

b-mehta committed 3 years ago

87b2e4ae

b-mehta committed 3 years ago

f2303b5b

b-mehta committed 3 years ago

2bd98d71

refactor(algebra/hom/group): Generalize `map_inv` to division monoids (#14134)

YaelDillies committed 3 years ago

844a4f7b

fix(tactic/core): Make the `classical` tactic behave like `open_locale classical` (#14122)

eric-wieser committed 3 years ago

90659cbe

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

Older