Commits leanprover-community/mathlib3

feat(number_theory/number_field/basic) : the ring of integers of a number field is not a field (#11956)

mariainesdff committed 4 years ago

edefc116

feat(measure_theory/function/ae_eq_of_integral): remove a few unnecessary `@` (#11974)

RemyDegenne committed 4 years ago

1b78b4d1

fix(algebra/monoid_algebra/basic): remove an instance that forms a diamond (#11918)

eric-wieser committed 4 years ago

114752ca

feat(model_theory/direct_limit): Direct limits of first-order structures (#11789)

awainverse committed 4 years ago

492393b0

feat(data/pi): provide `pi.mul_single` (#11849)

nomeata committed 4 years ago

024aef0b

fix(ring_theory/algebraic): prove a diamond exists and remove the instances (#11935)

eric-wieser committed 4 years ago

8c60a927

chore(data/real/ennreal, topology/instances/ennreal): change name of the order isomorphism for `inv` (#11959)

j-loreaux committed 4 years ago

fbfdff7e

chore(algebra/star): generalize star_bit0, add star_inv_of (#11951)

eric-wieser committed 4 years ago

ae14f6ad

feat(topology/algebra/group): added (right/left)_coset_(open/closed) (#11876)

Sebastian-Monnet committed 4 years ago

0227820c

refactor(order/well_founded, set_theory/ordinal_arithmetic): Fix namespace in `self_le_of_strict_mono` (#11871)

vihdzp committed 4 years ago

73513580

chore(number_theory/cyclotomic/zeta): generalize to primitive roots (#11941)

ericrbg committed 4 years ago

4a5728fe

feat(algebra/big_operators): add prod_multiset_count_of_subset (#11919)

Ruben-VandeVelde committed 4 years ago

d487230d

feat(algebra/module/basic): turn implications into iffs (#11937)

fpvandoorn committed 4 years ago

fb41da97

feat(group_theory/group_action/defs): add ext attributes (#11936)

eric-wieser committed 4 years ago

09293874

feat(analysis/inner_product_space/pi_L2): `map_isometry_euclidean_of_orthonormal` (#11907)

jsm28 committed 4 years ago

007d6602

feat(analysis/special_functions/complex/arg): `arg_mul`, `arg_div` lemmas (#11903)

jsm28 committed 4 years ago

923923f1

feat(group_theory/group_action/sub_mul_action): orbit and stabilizer lemmas (#11899)

AntoineChambert-Loir committed 4 years ago

1141703e

chore(algebra/punit_instances): all actions on punit are central (#11953)

eric-wieser committed 4 years ago

de707225

feat(category_theory): variants of Yoneda are fully faithful (#11950)

TwoFX committed 4 years ago

779d8363

feat(group_theory/subgroup/basic): `subgroup.map_le_map_iff_of_injective` (#11947)

tb65536 committed 4 years ago

80124455

feat(topology/subset_properties): more facts about compact sets (#11939)

urkud committed 4 years ago

c28dc84a

chore(field_theory/galois): make `intermediate_field.fixing_subgroup_equiv` computable (#11938)

eric-wieser committed 4 years ago

45ab382c

feat(category_theory/limits): epi equalizer implies equal (#11873)

TwoFX committed 4 years ago

a86277a2

feat(data/part): add instances (#11868)

BoltonBailey committed 4 years ago

20ef9097

feat(analysis/complex): add the Cauchy-Goursat theorem for an annulus (#11864)

urkud committed 4 years ago

3b9dc082

feat(order/conditionally_complete_lattice): `cInf_le` variant without redundant assumption (#11863)

vihdzp committed 4 years ago

efa31576

feat(number_theory/cyclotomic/gal): the Galois group of K(ζₙ) (#11808)

ericrbg committed 4 years ago

66d9cc1c

feat(group_theory/nilpotent): add nilpotent implies normalizer condition (#11586)

nomeata committed 4 years ago

1373d548

feat(algebra/group_power/basic): add lemmas about pow and neg on units (#11447)

eric-wieser committed 4 years ago

c3f6fce7

feat(category_theory/bicategory/functor_bicategory): bicategory structure on oplax functors (#11405)

yuma-mizuno committed 4 years ago

c3d87824