leanprover-community/mathlib

Pull Requests Commits

refactor(algebra/{group_power/{basic,lemmas},group_with_zero/power}): Generalize lemmas to division monoids (#14102)

YaelDillies committed 3 years ago

737784ef

feat(number_theory/legendre_symbol/*): move characters on `zmod n` to new file, add API, improve a proof (#14178)

MichaelStollBayreuth committed 3 years ago

89f2760f

chore(geometry/manifold/algebra/left_invariant_derivation): golf some proofs (#14172)

eric-wieser committed 3 years ago

93dca41a

refactor(data/pi/lex): Use `lex`, provide notation (#14164)

YaelDillies committed 3 years ago

4586a97a

feat(data/bool/basic): Kaminski's equation (#14159)

slerpyyy committed 3 years ago

009669cb

split(data/set/semiring): Split off `data.set.pointwise` (#14145)

YaelDillies committed 3 years ago

909b6732

feat(order/filter/at_top_bot): use weaker TC assumptions, add lemmas (#14105)

urkud committed 3 years ago

a9e74ab7

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

Newer Older