Commits leanprover-community/mathlib

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

feat (category_theory/karoubi_karoubi) : idempotence of karoubi (#11931)

joelriou committed 4 years ago

da164c6b

feat(algebra/lie/engel): add proof of Engel's theorem (#11922)

ocfnash committed 4 years ago

04909776

feat(set_theory/ordinal_arithmetic): More `lsub` and `blsub` lemmas (#11848)

vihdzp committed 4 years ago

f32fda7c

feat(group_theory/general_commutator): subgroup.prod commutes with the general_commutator (#11818)

nomeata committed 4 years ago

b7360f94

feat(algebra/order/hom/ring): Ordered semiring/ring homomorphisms (#11634)

YaelDillies committed 4 years ago

6afaf36d

feat(data/nat/factorization): bijection between positive nats and finsupps over primes (#11440)

stuart-presnell committed 4 years ago

8f5fd269

feat(set_theory/ordinal_arithmetic): The derivative of addition (#11270)

vihdzp committed 4 years ago

0aa0bc8f

feat(data/real/ennreal): `inv` is an `order_iso` to the order dual and lemmas for `supr, infi` (#11869)

j-loreaux committed 4 years ago

e60ca6b4

feat(measure_theory/probability_mass_function): Measure calculations for additional pmf constructions (#11858)

dtumad committed 4 years ago

b7e72ea4

chore(tactic/default): import `linear_combination` (#11942)

robertylewis committed 4 years ago

e9a18930

refactor(topology/algebra/mul_action2): rename type classes (#11940)

urkud committed 4 years ago

ea0e4589

feat(order/hom/bounded): Bounded order homomorphisms (#11806)

YaelDillies committed 4 years ago

4e8d8faa

doc(algebra/group/hom_instances): Fix spellings (#11943)

mans0954 committed 4 years ago

46911598

feat(topology/uniform_space/cauchy): add a few lemmas (#11912)

urkud committed 4 years ago

352e0642