leanprover-community/mathlib

Pull Requests Commits

Alternative definition of `form_perm`

Vierkantor committed 4 years ago

7c92eecb

Merge remote-tracking branch 'origin/master' into pechersky/form-perm-again

pechersky committed 4 years ago

4d34ef74

feat(ring_theory/hahn_series): extend the domain of a Hahn series by an `order_embedding` (#7551)

awainverse committed 4 years ago

3fd7cc36

feat(ring_theory/hahn_series): Hahn series form a field (#7495)

awainverse committed 4 years ago

81c98d5b

feat(analysis/normed_space/normed_group_hom): add lemmas (#7474)

riccardobrasca committed 4 years ago

1cbb31de

remove duplicate lemma

pechersky committed 4 years ago

a5b0a382

feat(algebra/lie/weights): add lemma `root_space_comap_eq_weight_space` (#7565)

ocfnash committed 4 years ago

b7ab74ab

chore(*): remove unnecessary `import tactic` (#7560)

kim-em committed 4 years ago

ac1f3df4

feat(data/int/basic): sign raised to an odd power (#7559)

tb65536 committed 4 years ago

17cba543

chore(deprecated/group): relax monoid to mul_one_class (#7556)

eric-wieser committed 4 years ago

3417ee07

feat(category_theory/limits/shapes/wide_pullbacks): Adds some wrappers around the (co)limit api for wide pullbacks/pushouts (#7546)

adamtopaz committed 4 years ago

477af65c

feat(data/list/rotate): is_rotated (#7299)

pechersky committed 4 years ago

92395fdf

chore(category_theory/Fintype): remove redundant lemmas (#7531)

jcommelin committed 4 years ago

41c7b1e3

feat(geometry/euclidean/triangle): add Stewart's Theorem + one similarity lemma (#7327)

manuelcandales committed 4 years ago

b9f4420c

feat(algebra/category/Module): Free R C, the free R-linear completion of a category (#7177)

kim-em committed 4 years ago

03b88c14

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

Merge branch 'master' into pechersky/form-perm-again

pechersky committed 4 years ago

f2880578

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

Older