Commits leanprover-community/mathlib

Finish last sorry!

Vierkantor committed 3 years ago

e91aedc1

Fill almost all holes

Vierkantor committed 3 years ago

a2a41b64

Merge remote-tracking branch 'mathlib/master' into ideal_norm

Vierkantor committed 3 years ago

f8c9d8a6

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

leanprover-community-bot committed 3 years ago

b5e9ffd2

feat(analysis/normed_space/operator_norm): variant of `continuous_linear_equiv.has_sum` (#15578)

ADedecker committed 3 years ago

6b34a400

feat(analysis/inner_product_space/basic): `orthonormal` version of `linear_independent.coe_range` (#15577)

ADedecker committed 3 years ago

8ab47c53

feat(combinatorics/simple_graph/connectivity): operations and lemmas about path type (#15156)

kmill committed 3 years ago

eece0d9b

feat(group_theory/subsemigroup/membership): add membership criteria for subsemigroups (#13945)

j-loreaux committed 3 years ago

3ce710a7

chore(tactic/*): clean up doc tags (#15563)

robertylewis committed 3 years ago

e1eba9fa

chore(algebra/module/injective): golf some proofs (#15534)

Ruben-VandeVelde committed 3 years ago

9696524a

feat(analysis/normed_space/linear_isometry): `linear_equiv.of_eq` as a `linear_isometry_equiv` (#15471)

ADedecker committed 3 years ago

34d4a9bf

feat(data/sum/order): `with_bot α ≃o punit ⊕ₗ α` and `with_top α ≃o α ⊕ₗ punit` (#15370)

vihdzp committed 3 years ago

de04bafa

feat(set_theory/zfc/basic): `Set.mem_insert → Set.mem_insert_iff`, add `Set.mem_insert` and `Set.mem_insert_of_mem` (#15573)

vihdzp committed 3 years ago

73cf56f1

feat(field_theory/adjoin): The compositum of finitely many finite dimensional intermediate fields is finite dimensional, finset version (#15426)

tb65536 committed 3 years ago

bff41725

feat(category_theory/preadditive): left exactness of certain hom functors (#15096)

TwoFX committed 3 years ago

9e4e72ae

feat(analysis/asymptotics): add `is_o*.of_pow` (#15568)

urkud committed 3 years ago

4eacd601

chore(measure_theory/measure/finite_measure_weak_convergence): golf (#15576)

Ruben-VandeVelde committed 3 years ago

08c1fbc7

refactor(analysis/special_functions/pow): assume `n ≠ 0` instead of `0 < n` (#15553)

urkud committed 3 years ago

c9f48402

feat(tactic/compute_degree + test/compute_degree): introduce a tactic for proving `f.(nat_)degree ≤ d` (#14762)

adomani committed 3 years ago

2f5afa10

feat(geometry/manifold): generalize some lemmas from `smooth` to `cont_mdiff` (#15560)

urkud committed 3 years ago

382acc15

refactor(logic/encodable/small): migrate to `countable` (#15557)

urkud committed 3 years ago

6fed0370

feat(data/nat/pairing): basic bounds on `mkpair` (#15539)

vihdzp committed 3 years ago

0c79da05

feat(analysis/normed*): add instances and lemmas (#15515)

urkud committed 3 years ago

ebf73435

refactor(order/boolean_algebra): Get rid of `boolean_algebra.core` (#15302)

YaelDillies committed 3 years ago

3838b0e0

feat(data/sym/basic): combinatorial equivalence for `sym (option α) n.succ` (#15192)

kmill committed 3 years ago

f01c132b

refactor(data/nat/factorization): Change definition of `factorization` to be computable (#12301)

BoltonBailey committed 3 years ago

80ae52a9

feat(order/succ_pred/basic): `succ_le_succ_iff`, etc. taking `¬ is_max` hypotheses (#15536)

vihdzp committed 3 years ago

c26a844f

feat(tactic/attribute): add `expand_exists` (#15498)

0x182d4454fb211940 committed 3 years ago

f9153b8a

refactor(order/rel_classes): ditch `is_extensional` (#15373)

vihdzp committed 3 years ago

1dd65b6a

feat(set_theory/ordinal/basic): dot notation lemmas + golf (#15348)

vihdzp committed 3 years ago

309f7594