Commits leanprover-community/mathlib3

feat(analysis/inner_product_space/projection): various facts about `orthogonal_projection` (#15807)

ADedecker committed 3 years ago

2f9a7218

chore(linear_algebra/free_module/basic): tidy up (#15956)

eric-wieser committed 3 years ago

f37e88f3

feat(analysis/normed/field/basic): define `densely_normed_field` give instances for ℚ, ℝ, ℂ and `is_R_or_C` (#15657)

j-loreaux committed 3 years ago

b6ab1f47

feat(number_theory/number_field.lean): generalise ```range_eq_roots``` to relative extensions (#15903)

xroblot committed 3 years ago

77d020f7

feat(number_theory/legendre_symbol/quadratic_char): add results on special values (#15888)

MichaelStollBayreuth committed 3 years ago

4a1b5307

refactor(algebra/periodic): weaken another `antiperiodic` typeclass assumption (#15961)

jsm28 committed 3 years ago

59eef0a2

fix(geometry/manifold/complex): remove nonempty assumption (#15948)

jcommelin committed 3 years ago

5e0a5bc6

chore(probability/*): change to probability notation in the probability folder (#15933)

kex-y committed 3 years ago

a150b69f

chore(data/polynomial/induction): cleanup (#15918)

eric-wieser committed 3 years ago

d4b56199

feat(algebra/order/archimedean): `archimedean_iff_int_lt`, `archimedean_iff_int_le`, `floor_ring.archimedean` (#15909)

jsm28 committed 3 years ago

df1179db

feat(algebra/algebra/operations): pointwise mul_semiring_action on submodules (#15877)

eric-wieser committed 3 years ago

bc1341f6

feat(group_theory/group_action/conj_act): smul_comm_class instances (#15876)

eric-wieser committed 3 years ago

71320d9b

chore(measure_theory/function/condexp): split `conditional_expectation` into multiple files (#15714)

kex-y committed 3 years ago

878370b7

feat(set_theory/zfc): lemmas on `to_set` (#15265)

vihdzp committed 3 years ago

b88fa08f

chore(algebra/order/floor): generalize lemmas about adding nat from rings to semirings (#15952)

eric-wieser committed 3 years ago

eb55b1e9

feat(algebra/hom/group_instances): add missing `int_cast` and `nat_cast` lemmas to `add_monoid.End` and `module.End` (#15839)

eric-wieser committed 3 years ago

f028ff2b

feat(analysis/convex/cone): lemmas about `inner_dual_cone` of unions (#15836)

eric-wieser committed 3 years ago

1a51c706

feat(data/list/perm): binding all the sublists of a given length gives all the sublists (#15834)

eric-wieser committed 3 years ago

75f5289e

feat(measure_theory/measure/measure_space): add instance `compact_space.is_finite_measure` (#15693)

ocfnash committed 3 years ago

545a5953

feat(analysis/special_functions/trigonometric/angle): more `sin` and `cos` lemmas (#15945)

jsm28 committed 3 years ago

7adef571

refactor(algebra/periodic): weaken `antiperiodic` typeclass assumptions (#15941)

jsm28 committed 3 years ago

d812abd8

fix(number_theory/cyclotomic/primitive_roots): speedup (#15804)

ericrbg committed 3 years ago

346cc93c

feat(algebra/periodic): `const_add`, `add_const`, `const_sub`, `sub_const` (#15782)

jsm28 committed 3 years ago

954f3e16

feat(algebra/category/Group/epi_mono): (mono)epimorphisms and (in)surjections are the same in `(Add)(Comm)Group` (#15496)

jjaassoonn committed 3 years ago

b74907b6

feat(analysis/convex): the gauge as a seminorm over is_R_or_C (#14879)

mcdoll committed 3 years ago

a88bc4f7

feat(category_theory/limits): the constant functor preserves (co)limits (#15938)

TwoFX committed 3 years ago

03f58c52

feat(algebra/big_operators/basic): Sums and product in `additive`/`multiplicative` (#15898)

YaelDillies committed 3 years ago

26e8026f

feat(topology/algebra/group): add lemmas about `units` (#15921)

urkud committed 3 years ago

0bd4faee

feat(geometry/manifold/complex): holomorphic function on compact connected manifold is constant (#15667)

hrmacbeth committed 3 years ago

ec818836

doc(algebra/homology/homological_complex): fix doc and names (#15940)

riccardobrasca committed 3 years ago

e0b90625