Commits leanprover-community/mathlib3

feat(number_theory/cyclotomic/rat): add integral_power_basis (#15570)

riccardobrasca committed 3 years ago

16cf14f1

feat(category_theory/limits): bundled exact functors (#12336)

TwoFX committed 3 years ago

9fc53308

feat(algebraic_topology/dold_kan): construction of an idempotent endomorphism (#15950)

joelriou committed 3 years ago

3dbd6809

feat(category_theory/generator): complete well-powered category with small coseparating set has an initial object (#15865)

TwoFX committed 3 years ago

952e7ee9

feat(category_theory/limits): transport has_initial across equivalences (#15858)

TwoFX committed 3 years ago

ea74dc9f

feat(geometry/manifold/cont_mdiff): more flexibility in changing charts (#15519)

fpvandoorn committed 3 years ago

4ef4fefe

feat(category_theory/abelian): equivalence between subobjects and quotients (#15494)

TwoFX committed 3 years ago

be63ea29

feat(topology/local_at_target): Properties of continuous maps that are local at the target. (#15452)

erdOne committed 3 years ago

d8510cac

feat(topology/connected): make `connected_component_in` more usable, develop API (#15964)

ADedecker committed 3 years ago

a4ea8895

feat(logic/equiv/list): add `countable` instances (#15960)

urkud committed 3 years ago

d4805efb

feat(analysis/calculus/cont_diff): Add `cont_diff` lemmas for constant scalar multiplication (#15895)

mcdoll committed 3 years ago

30cf3db4

feat(analysis/inner_product_space/l2_space): define `is_hilbert_sum` predicate (#15772)

ADedecker committed 3 years ago

0e0a8b42

feat(field_theory/adjoin): `intermediate_field.adjoin` equals `subalgebra.adjoin` for algebraic sets (#15762)

tb65536 committed 3 years ago

73421d52

feat(data/polynomial/ring_division,ring_theory/algebraic): Basic consequences of `x ∈ p.root_set` (#15745)

tb65536 committed 3 years ago

0fb4144a

feat(data/nat/totient): add lemma `totient_dvd_of_dvd` (#15642)

stuart-presnell committed 3 years ago

7c205ffb

feat(ring_theory/integral_closure): finite = integral + finite_type (#15970)

erdOne committed 3 years ago

b5eb0429

feat(topology/nhds_set): add several lemmas (#15957)

urkud committed 3 years ago

f7534de0

chore(data/polynomial/degree/definitions): make an argument explicit (#15951)

adomani committed 3 years ago

94a20a74

refactor(data/fintype/basic): drop 2 noncomputable instances (#15943)

urkud committed 3 years ago

36d300ce

feat(topology/instances/sign): topology of `sign_type` and `sign` (#15925)

jsm28 committed 3 years ago

1cdd8266

chore(topology/*): Use `finite` in place of `fintype` where possible (#15891)

YaelDillies committed 3 years ago

d38aca11

feat(algebraic_geometry/morphisms/basic): Basic framework for local properties of morphisms. (#15709)

erdOne committed 3 years ago

af80234d

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