Commits leanprover-community/mathlib3

first commit

erdOne committed 3 years ago

8eac6e72

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

leanprover-community-bot committed 3 years ago

2792268f

chore(*/..eq): add is_refl instances (#15963)

ericrbg committed 3 years ago

146d3d1f

feat(analysis/convex/cone): add `convex_cone.strictly_positive` and monotonicity lemmas (#15837)

eric-wieser committed 3 years ago

cad35c79

feat(order/initial_seg): `is_empty (r ≺i r)` (#15803)

vihdzp committed 3 years ago

f838fe85

chore(order/filter): move `filter.prod` and `filter.coprod` to a new file (#15937)

urkud committed 3 years ago

a913b9b4

feat(order/max): no value is accessible in a `no_min_order` / `no_max_order` (#15931)

vihdzp committed 3 years ago

e71c115f

chore(analysis/calculus/cont_diff): rename and add @[simp] to `iterated_fderiv_within_zero_fun` (#15896)

mcdoll committed 3 years ago

511caf6a

chore(analysis/calculus/cont_diff): Add two helper lemmas (#15894)

mcdoll committed 3 years ago

a5413b69

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