Commits leanprover-community/mathlib3

feat(geometry/euclidean/angle/oriented/basic): `inner_eq_zero` lemmas (#17265)

jsm28 committed 3 years ago

34d8782b

feat(geometry/euclidean/angle/oriented/affine): signs of angles and sides of subspaces (#17234)

jsm28 committed 3 years ago

35ca0862

feat(group_theory/transfer): Prove Burnside's transfer theorem (#17263)

tb65536 committed 3 years ago

d3731988

chore(ring_theory/ideal/local_ring): use `derive` for more consistent instances (#17468)

eric-wieser committed 3 years ago

d1accf4f

feat(topology/algebra/module/finite_dimension): add `linear_map.is_open_map_of_finite_dimensional` (#17466)

urkud committed 3 years ago

c6c8f200

doc(undergrad.yaml): representation theory (#17459)

antoinelab01 committed 3 years ago

c005eac4

doc(overview.yaml): representation theory (#17458)

antoinelab01 committed 3 years ago

8d9f31db

feat(group_theory/order_of_element): lemmas about orders of powers of group elements (#17433)

ocfnash committed 3 years ago

ac825bfa

chore(data/nat/prime): add 2 aliases (#17372)

urkud committed 3 years ago

c946d609

feat(linear_algebra/dual): more about `dual_annihilator` (#17313)

kmill committed 3 years ago

c9b80414

feat(ring_theory/dedekind_domain): lemmas on inequality between ideal powers (#17188)

Vierkantor committed 3 years ago

20c144b5

feat(analysis/normed{_space/basic, /field/basic}): add some induced norm structures on subobjects (#17169)

j-loreaux committed 3 years ago

089f741b

feat(group_theory/submonoid/membership): +2 induction principles (#17160)

urkud committed 3 years ago

95e5153a

feat(algebra/ring/equiv): add lemma on coercion to equivs and symm (#17101)

alexjbest committed 3 years ago

642809e9

refactor(analysis/convex/strict): rename, golf, generalize (#17464)

urkud committed 3 years ago

9709d60a

refactor(topology/sequences): golf, review API (#17454)

urkud committed 3 years ago

aae8d563

feat(set_theory/ordinal/{basic, arithmetic}): move basic results earlier (#15801)

vihdzp committed 3 years ago

27863065

feat(ring_theory/non_unital_subsemiring/basic): introduce non-unital subsemirings and develop basic API (#13749)

j-loreaux committed 3 years ago

3711afe1

refactor(*): simplifying import hierarchy up to dat.rat.order (#17435)

kim-em committed 3 years ago

cead9313

feat(analysis/normed_space/spectrum): lemmas about spectral radius, spectral mapping and `alg_hom_class` maps into the base field (#17178)

j-loreaux committed 3 years ago

ef61778b

feat(data/pfun): review APIs, add some lemmas about `fix_induction` (#17004)

astrainfinita committed 3 years ago

13bc7a20

chore(data/fintype/basic): don't reimplement finset.map (#17460)

eric-wieser committed 3 years ago

52d7570d

feat(data/nat/gcd/basic): add `nat.dvd_mul` and `dvd_mul` (#17131)

eric-wieser committed 3 years ago

b7a54188

chore(data/finsupp/defs): redefine `finsupp.single` as `pi.single` (#17356)

eric-wieser committed 3 years ago

d61f638a

feat(number_theory/divisors): more thoroughly link `divisors_antidiagonal` and `divisors` (#17050)

eric-wieser committed 3 years ago

c66f2aee

feat(algebra/*): add coercions from hom classes to their respective homs (#17000)

j-loreaux committed 3 years ago

dfd46033

chore(topology/fiber_bundle): move trivializations to a new file (#17463)

hrmacbeth committed 3 years ago

0b00e53a

feat(topology/algebra/const_mul_action): support of a function composed with smul (#17456)

sgouezel committed 3 years ago

18b38810

feat(tactic/move_add, test/move_add): a tactic for moving around summands (#13483)

adomani committed 3 years ago

e8b1a293

feat(analysis/convolution): weaken typeclass assumptions (#17452)

sgouezel committed 3 years ago

262dfc94