leanprover-community/mathlib3

Pull Requests Commits

refactor(linear_algebra/charpoly): split file to reduce imports (#13778)

kim-em committed 4 years ago

0009ffba

refactor(algebra/restrict_scalars): remove global instance on module_orig (#13759)

kim-em committed 4 years ago

dd4590af

fix(src/tactic/alias): Teach `get_alias_target` about `alias f ↔ a b` (#13742)

nomeata committed 4 years ago

abcd601c

feat(data/int/cast): int cast division lemmas (#13929)

b-mehta committed 4 years ago

0038a043

feat(set_theory/game/birthday): More basic lemmas on birthdays (#13729)

vihdzp committed 4 years ago

46023701

feat(group_theory/complement): API lemmas relating `range_mem_transversals` and `to_equiv` (#13694)

tb65536 committed 4 years ago

60ad8448

feat(group_theory/free_group): is_free_group via `free_group X ≃* G` (#13633)

nomeata committed 4 years ago

923ae0bc

feat(number_theory/cyclotomic/rat): the ring of integers of cyclotomic fields. (#13585)

riccardobrasca committed 4 years ago

552a4709

feat(algebra/homology/Module): API for complexes of modules (#12622)

kim-em committed 4 years ago

e7161393

feat(set_theory/cardinal/cofinality): Cofinality of normal functions (#12384)

vihdzp committed 4 years ago

a7c50973

feat(analysis/convex/topology): Separating by convex sets (#11458)

YaelDillies committed 4 years ago

d565adb7

feat(measure_theory/integral/lebesgue): speed up a proof (#13946)

sgouezel committed 4 years ago

32320a10

fix(ring_theory/polynomial/basic): fix unexpected change of an implicit parameter (#13935)

astrainfinita committed 4 years ago

ceca8d74

feat(linear_algebra/span): add `finite_span_is_compact_element` (#13901)

haruhisa-enomoto committed 4 years ago

53c79d56

feat(order/basic): Notation for `order_dual` (#13798)

YaelDillies committed 4 years ago

a057441e

feat(linear_algebra/prod): linear version of prod_map (#13751)

antoinelab01 committed 4 years ago

402e5647

feat(order/well_founded): Well founded relations are asymmetric and irreflexive (#13692)

vihdzp committed 4 years ago

e1f00bc7

feat(algebra/module/torsion): torsion ideal, decomposition lemma (#13414)

pbazin committed 4 years ago

6c7b880e

move(set_theory/ordinal/{arithmetic → fixed_points}): Move `nfp` (#13315)

vihdzp committed 4 years ago

e24f7f7a

feat(measure_theory/function/l1_space): add `integrable_smul_measure` (#13922)

urkud committed 4 years ago

1a862493

chore(ring_theory/polynomial/basic): golf polynomial_not_is_field (#13919)

Ruben-VandeVelde committed 4 years ago

af4c6c8a

feat(data/finset/prod): diag of union (#13916)

b-mehta committed 4 years ago

d0efe252

feat(category_theory/simple): nonzero morphisms to/from a simple are epi/mono (#13905)

kim-em committed 4 years ago

098ab17f

refactor(group_theory/{submonoid, subsemigroup}/{center, centralizer}): move set.center and set.centralizer into subsemigroup (#13903)

j-loreaux committed 4 years ago

455393d3

feat(ring_theory/valuation/valuation_subring): Adds some equivalent conditions for equivalence of valuations (#13895)

adamtopaz committed 4 years ago

e6b84992

feat(data/list/basic): add `list.cons_diff` (#13892)

urkud committed 4 years ago

6d370064

feat(analysis/matrix): add `frobenius_norm_conj_transpose` (#13883)

eric-wieser committed 4 years ago

269bc85d

feat(category_theory/simple): simple objects are indecomposable (#13882)

kim-em committed 4 years ago

d537897a

feat(linear_algebra/trace): more general versions of `trace_mul_comm` and `trace_conj` (#13874)

antoinelab01 committed 4 years ago

1afdaf96

feat(topology/algebra/star): continuity of `star` (#13855)

eric-wieser committed 4 years ago

517aa8b6

Newer Older