leanprover-community/mathlib3

Pull Requests Commits

refactor(subgroup/basic): use `subgroup.subgroup_of` as the normal form (#17744)

urkud committed 3 years ago

d57133e4

feat(algebra/order/to_interval_mod): lemmas about changing the base of the period (#17741)

eric-wieser committed 3 years ago

2aa04f65

feat(category_theory): is_zero.op and is_zero.unop (#17718)

joelriou committed 3 years ago

74333bd5

feat(algebra/group_with_zero/defs): add is_cancel_mul_zero (#17716)

riccardobrasca committed 3 years ago

4b240be0

refactor(algebraic_geometry/EllipticCurve): refactor base change and variable change (#17708)

Multramate committed 3 years ago

73aaf32e

feat(ring_theory): `is_adjoin_root` predicate (#17690)

Vierkantor committed 3 years ago

81fb9f8f

chore(data/rat/cast): split (#17761)

hrmacbeth committed 3 years ago

23f67f2f

chore(algebra/order/hom/basic): move positivity extension (#17758)

hrmacbeth committed 3 years ago

62a56268

chore(data/list/zip): add some lemmas about zip_with3 (#17498)

eric-wieser committed 3 years ago

61e34d5e

chore(data/nat/basic): split out even_odd_rec (#17759)

kim-em committed 3 years ago

306801e1

feat(measure_theory/group/add_circle): fundamental domain for rational angle rotations in the circle (#17462)

ocfnash committed 3 years ago

fa71e713

feat(algebra/order/floor): sub/super-additivity of floor/ceil/fract (#17728)

eric-wieser committed 3 years ago

0926481d

chore(scripts/port_status): reuse the parser from mathlibtools (#17620)

eric-wieser committed 3 years ago

11649045

feat(analysis/convex/between): `wbtw_line_map_iff`, `sbtw_line_map_iff` (#17685)

jsm28 committed 3 years ago

cb48031c

feat(measure_theory/group/action): `smul_invariant_measure` instances (#17590)

YaelDillies committed 3 years ago

10079b92

feat(geometry/euclidean/angle/oriented/basic): angles and spans of vectors (#17525)

jsm28 committed 3 years ago

260f0788

feat(group_theory/subgroup/basic): generalize `monoid_hom.eq_locus` (#17748)

urkud committed 3 years ago

4f81077a

chore(algebra/order/to_interval_mod): add `equiv` versions extracted from `add_circle` (#17739)

eric-wieser committed 3 years ago

fc6ece0a

feat(order/upper_lower): `×ˢ` notation for upper/lower sets (#17746)

YaelDillies committed 3 years ago

4e42a9d0

feat(linear_algebra/affine_space/affine_map): `line_map_injective` (#17735)

jsm28 committed 3 years ago

ed71500f

feat (data/sign): `sign_sum` (#17657)

jsm28 committed 3 years ago

57345aed

refactor(data/polynomial/degree/definitions): Remove duplicate lemma (#17740)

tb65536 committed 3 years ago

a00186d7

ci(scripts/add_port_comments): deal with files that have no module docstring to edit (#17737)

eric-wieser committed 3 years ago

f2f23df7

chore(*): revert #17048 (#17733)

kim-em committed 3 years ago

a148d797

feat(data/list/basic): index of element in appended lists (#17720)

madvorak committed 3 years ago

22feff54

feat(measure_theory/integral/lebesgue): Add Markov inequalities for tsum and card using counting measure. (#17588)

kkytola committed 3 years ago

3891ab62

feat(algebra/module/composition_series): Jordan-Hölder for modules (#17295)

MadPidgeon committed 3 years ago

cce7f68a

chore(*): add mathlib4 synchronization comments (#17736)

github-actions[bot] committed 3 years ago

1fc36cc9

chore(order/bounded_order): split (#17730)

kbuzzard committed 3 years ago

97be0de9

chore(scripts/port_status.py): don't list default.lean (#17725)

kim-em committed 3 years ago

853d148d

Newer Older