Commits leanprover-community/mathlib3

feat(algebra/star): allow star_module to be used on non-commutative rings

eric-wieser committed 4 years ago

d5f356aa

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

feat(topology/continuous_function/bounded): register instances of `star` structures (#10570)

j-loreaux committed 4 years ago

e618cfe3

fix(tactic/ring): instantiate metavariables (#10589)

digama0 committed 4 years ago

25386262

feat(algebra/algebra/spectrum): lemmas when scalars are a field (#10476)

j-loreaux committed 4 years ago

94783bef

feat(data/finsupp/basic): lemmas on the support of the `tsub` of `finsupp`s (#10651)

stuart-presnell committed 4 years ago

08215b55

feat(measure_theory/integral/set_to_l1): properties of (dominated_)fin_meas_additive (#10590)

RemyDegenne committed 4 years ago

9ef122d2

feat(group_theory/submonoid): The monoid_hom from a submonoid to its image. (#10680)

erdOne committed 4 years ago

c23b54c7