leanprover-community/mathlib3

Pull Requests Commits

eric-wieser committed 4 years ago

4d595c72

chore(group_theory/group_action/group): add `smul_inv`

eric-wieser committed 4 years ago

4da091fc

feat(data/set/lattice): (b)Union and (b)Inter lemmas (#7557)

PatrickMassot committed 4 years ago

48104c3a

feat(data/matrix/basic): add missing smul instances, generalize lemmas to work on scalar towers (#7544)

eric-wieser committed 4 years ago

b5776971

feat(field_theory/abel_ruffini): Version of solvable_by_rad.is_solvable (#7509)

tb65536 committed 4 years ago

38bf2abd

refactor(*): bundle `is_basis` (#7496)

Vierkantor committed 4 years ago

ef90a7ab

feat(group_theory/subgroup): add mem_map_of_mem (#7459)

riccardobrasca committed 4 years ago

f985e364

feat(data/equiv/basic): equiv.curry (#7458)

jcommelin committed 4 years ago

4a8467a4

refactor(ring_theory/localization): Golf two proofs (#7520)

justus-springer committed 4 years ago

7150c90f

feat(topology): tiny new lemmas (#7554)

PatrickMassot committed 4 years ago

ea0043ca

chore(group_theory): some new convenience lemmas (#7555)

PatrickMassot committed 4 years ago

735a26e5

feat(uniform_space/cauchy): cauchy_seq lemmas (#7528)

PatrickMassot committed 4 years ago

581064fd

feat(topology/metric_space/basic): dist_ne_zero (#7552)

benjamindavidson committed 4 years ago

bf229dd5

feat(algebra/lie/weights): define weight spaces of Lie modules (#7537)

ocfnash committed 4 years ago

132328c4

feat(topology/subset_properties, homeomorph): lemmata about embeddings (#7431)

AlexKontorovich committed 4 years ago

4a8a5950

feat(algebraic_geometry/structure_sheaf): Structure sheaf on basic opens (#7405)

justus-springer committed 4 years ago

583ad823

feat(topology/category/*): Add alternative explicit limit cones for `Top`, etc. and shows `X : Profinite` is a limit of finite sets. (#7448)

adamtopaz committed 4 years ago

dbcd4546

feat(group_theory/perm/*): lemmas about `extend_domain`, `fin_rotate`, and `fin.cycle_type` (#7447)

awainverse committed 4 years ago

515fb2f0

feat(ring_theory/hahn_series): order of a nonzero Hahn series, reindexing summable families (#7444)

awainverse committed 4 years ago

5cfcb6a0

feat(topology/uniform_space): is_closed_of_spread_out (#7538)

PatrickMassot committed 4 years ago

72e151d8

feat(group_theory.quotient_group): add eq_iff_div_mem (#7523)

riccardobrasca committed 4 years ago

301542a4

feat(field_theory/polynomial_galois_group): More flexible version of gal_action_hom_bijective_of_prime_degree (#7508)

tb65536 committed 4 years ago

63a17823

feat(data/nat/cast): pi.coe_nat and pi.nat_apply (#7492)

jcommelin committed 4 years ago

565310f1

feat(algebra/module/basic): smul_add_hom_one (#7461)

jcommelin committed 4 years ago

190d4e28

feat(category_theory/arrow): arrow.mk_inj (#7456)

jcommelin committed 4 years ago

91d5aa6b

refactor(*): more choice-free proofs (#7455)

digama0 committed 4 years ago

6fc8b2a9

feat(group_theory/solvable): S_5 is not solvable (#7453)

tb65536 committed 4 years ago

dec29aa3

refactor(group_theory/perm/*): disjoint and support in own file (#7450)

pechersky committed 4 years ago

95b91b38

feat(ring_theory/finiteness): add monoid_algebra.ft_iff_fg (#7445)

riccardobrasca committed 4 years ago

251a42b5

feat(linear_algebra/quadratic_form): provide `distrib_mul_action S (quadratic_form M R)` when `S` has no addition. (#7443)

eric-wieser committed 4 years ago

be1af7ce

Older