leanprover-community/mathlib3

Pull Requests Commits

feat(measure_theory): integral is mono in measure (#10721)

urkud committed 4 years ago

f9fff7c6

feat(group_theory/submonoid): The submonoid of left inverses of a submonoid (#10679)

erdOne committed 4 years ago

cc5ff8ca

feat(ring_theory/polynomial/cyclotomic/eval): `cyclotomic_pos` (#10482)

ericrbg committed 4 years ago

1c2b7420

refactor(algebra/group/basic): Migrate add_comm_group section into comm_group section (#10565)

mans0954 committed 4 years ago

f068b9de

Fix comment typo (#10715)

berndlosert committed 4 years ago

294753e9

feat(analysis/normed_space): normed space is homeomorphic to the unit ball (#10690)

urkud committed 4 years ago

97417665

chore(algebra/pointwise): Better `variables` management (#10686)

YaelDillies committed 4 years ago

08d30d66

feat(ring_theory/localization): Clearing denominators (#10668)

erdOne committed 4 years ago

d856bf9b

chore(algebra/group_with_zero/defs: Rename `comm_cancel_monoid_with_zero` to `cancel_comm_monoid_with_zero` (#10669)

YaelDillies committed 4 years ago

0b87b0ae

docs(topology/homotopy): add namespace in docstring to fix links (#10711)

ADedecker committed 4 years ago

52c2f742

feat(logic/function/basic): surjective function is an epimorphism (#10691)

urkud committed 4 years ago

a12fc705

feat(algebra/gcd_monoid): `associates` lemmas (#10705)

ericrbg committed 4 years ago

3e1d4d32

feat(ring_theory/discriminant): add the discriminant of a family of vectors (#10350)

riccardobrasca committed 4 years ago

b7ac8334

feat(order/basic): Slightly generalized `densely_ordered` (#10664)

vihdzp committed 4 years ago

71e9f90d

feat(data/nat/gcd): coprime add mul lemmas (#10588)

BoltonBailey committed 4 years ago

12e18e8e

feat(group_theory/group_action/defs): add a typeclass to show that an action is central (aka symmetric) (#10543)

eric-wieser committed 4 years ago

18ce3a8f

chore(algebraic_geometry/presheafed_space): Make `has_colimits` work faster (#10703)

erdOne committed 4 years ago

94d51b99

feat(data/int/gcd): another version of Euclid's lemma (#10622)

stuart-presnell committed 4 years ago

c29b7067

feat(order/lattice): define a lattice structure using an injective map to another lattice (#10615)

RemyDegenne committed 4 years ago

4471de61

feat(ring_theory/principal_ideal_domain): add some corollaries about is_coprime (#10601)

Ruben-VandeVelde committed 4 years ago

ebbb991a

feat(*): introduce classes for types of homomorphism (#9888)

Vierkantor committed 4 years ago

46ac3c41

refactor(group_theory/quotient_group): use `con` (#10699)

urkud committed 4 years ago

165e0556

chore(ring_theory/noetherian): rename `submodule.fg_map` to `submodule.fg.map` (#10688)

eric-wieser committed 4 years ago

9a24b3e5

feat(ring_theory/polynomial/cyclotomic): generalize `is_root_cyclotomic` (#10687)

ericrbg committed 4 years ago

24cf723e

feat(group_theory/finiteness): Lemmas about finitely generated submonoids (#10681)

erdOne committed 4 years ago

3dcdf93f

feat(ring_theory/ideal): Power of a spanning set is a spanning set (#10656)

erdOne committed 4 years ago

508fc181

feat(category_theory/limits): Pullback API (#10620)

erdOne committed 4 years ago

ce0e2c44

chore(scripts): update nolints.txt (#10697)

leanprover-community-bot committed 4 years ago

e7959fb8

chore(algebra/punit_instances): add `comm_cancel_monoid_with_zero`, `normalized_gcd_monoid`, and scalar action instances (#10312)

eric-wieser committed 4 years ago

1ecdf714

feat(probability_theory/martingale): define martingales (#10625)

RemyDegenne committed 4 years ago

61dd3432

Newer Older