Commits leanprover-community/mathlib3

feat(data/matrix/basic): Add `alg_equiv` and `linear_equiv` instances for transpose. (#15386)

linesthatinterlace committed 3 years ago

d244509f

feat(*/partition_of_unity): more lemmas based on the partition of unity (#15609)

urkud committed 3 years ago

168d6ba8

feat(category_theory/preadditive/*): algebra over endofunctor preadditive and forget additive functor (#15100)

Julian-Kuelshammer committed 3 years ago

f5138d15

fix(algebraic_geometry/projective_spectrum/scheme) : fix module doc string (#15633)

jjaassoonn committed 3 years ago

62a1f82f

feat(algebraic_geometry/morphisms): Basic framework for classes of morphisms between schemes (#14944)

erdOne committed 3 years ago

b351ad53

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

leanprover-community-bot committed 3 years ago

44c1fdca

chore(algebra/module/basic): use `simp` instead of `norm_num` (#15670)

urkud committed 3 years ago

48dec300

chore(algebra/order/sub): Generalize lemmas (#15497)

YaelDillies committed 3 years ago

5f543bd9

feat(analysis/normed_space/lp_space): construct star structures on lp spaces (#15317)

JonBannon committed 3 years ago

3419dfc0

refactor(set_theory/ordinal/basic): `ordinal.min` → `infi` (#14707)

vihdzp committed 3 years ago

a1ce53c0

feat(representation_theory/Rep): Rep k G ≌ Module (monoid_algebra k G) (#13713)

kim-em committed 3 years ago

5ed2c728

feat(algebra/periodic): `fract_periodic` (#15660)

jsm28 committed 3 years ago

86febe13

feat(order/bounded_order): an order is either an `order_bot` or a `no_bot_order` (#15636)

vihdzp committed 3 years ago

75f10446

feat(linear_algebra/tensor_product): add id_apply and comp_apply for ltensor and rtensor (#15628)

kbuzzard committed 3 years ago

a1fdc999

refactor(data/{finite,fintype}): move some lemmas to `data.fintype.basic` (#15626)

urkud committed 3 years ago

aed4c494

chore(*): Rename `normed_group` to `normed_add_comm_group` (#15619)

YaelDillies committed 3 years ago

d1bd9c5d

feat(set_theory/zfc/basic): `∈` is well-founded on classes (#15544)

vihdzp committed 3 years ago

989fe520

feat(data/list/of_fn): lemmas to turn quantifiers over lists to quantifiers over tuples (#15433)

eric-wieser committed 3 years ago

639fe5ab

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

leanprover-community-bot committed 3 years ago

b3bcb796

feat(analysis/normed_space/linear_isometry): add defs and lemmas (#15650)

urkud committed 3 years ago

4a4c2753

feat(analysis/inner_product_space/positive): definition and basic facts about positive operators (#15470)

ADedecker committed 3 years ago

0179605f

feat(number_theory/legendre_symbol/add_character): add file introducing additive characters (#15499)

MichaelStollBayreuth committed 3 years ago

983c737a

fix(*): fix typos I made yesterday (#15627)

urkud committed 3 years ago

c9ba943d

refactor(*): rename `nondiscrete_normed_field` (#15625)

j-loreaux committed 3 years ago

ef901ea6

refactor(data/set/countable): golf using `_root_.countable`, review API (#15624)

urkud committed 3 years ago

4050b906

chore(algebra/lie/direct_sum): remove `direct_sum.lie_algebra_is_internal` (#15631)

eric-wieser committed 3 years ago

c0cc689b

feat(data/finset/basic): There is exactly one set in empty types (#15607)

YaelDillies committed 3 years ago

92e96605

feat(order/partition/finpartition): Bound size of a bit of `finpartition.atomise` (#15350)

YaelDillies committed 3 years ago

6537ae9c

feat(combinatorics/simple_graph/density): Bound on the difference between edge densities (#15353)

YaelDillies committed 3 years ago

7c94fe71

feat(ring_theory/noetherian): Finitely generated idempotent ideal is principal. (#15561)

erdOne committed 3 years ago

106f0ac9