This repository has been archived by the owner on Jul 24, 2024. It is now read-only.
feat(tactic/polyrith): solve more problems by testing for membership in the radical#15425
Closed
robertylewis wants to merge 177 commits intomasterfrom polyrith-radical
+113-52
Commits
Commits on Jul 16, 2022
- committed
- committed
Commits on Jul 22, 2022
Commits on Aug 1, 2022
feat(analysis/locally_convex/with_seminorms): in a normed space, von Neumann bounded = metric bounded (#15124)
feat(number_theory/legendre_symbol/add_character): add file introducing additive characters (#15499)
feat(analysis/inner_product_space/positive): definition and basic facts about positive operators (#15470)
feat(algebraic_geometry/morphisms): Basic framework for classes of morphisms between schemes (#14944)
feat(category_theory/preadditive/*): algebra over endofunctor preadditive and forget additive functor (#15100)
feat(linear_algebra/annihilating_polynomial): add definition of annihilating ideal and show minpoly generates in field case (#12140)
refactor(measure_theory/function/uniform_integrable): change
uniform_integrableto only requireae_strongly_measurable(#15623)feat(measure_theory/measure/finite_measure_weak_convergence): Add normalization of finite measures to probability measures and characterize weak convergence in terms of it. (#15528)
- committed
feat(measure_theory/function/conditional_expectation): pull-out property of the conditional expectation (#15274)
feat(measure_theory/constructions/borel_space): the set of points for which a measurable sequence of functions converges is measurable (#15307)
feat(ring_theory/valuation/valuation_subring): define maximal ideal of valuation subring and provide basic API (#14656)
refactor(topology/algebra/order/basic): Add antitone versions of sup and inf lemmas for continuous monotone functions and move them to monotone/antitone namespaces. (#15218)
feat(category_theory/preadditive): constructing a semiadditive structure from binary biproducts (#14445)
feat(linear_algebra/basis): shows the lattice of submodules of a module over a division ring is atomistic (#14883)
feat(category_theory/limits/construction): Construct finite limits from terminal objects and pullbacks (#14948)
feat(ring_theory): Formally étale/smooth/unramified morphisms are stable under base change. (#15243)
doc(field_theory/splitting_field): update code example to reflect changes to diamond issues (#15620)
feat(probability/martingale): the discrete stochastic integral of a submartingale is a submartingale (#14909)
chore(topology/algebra/module, analysis/normed_space/linear_isometry): dedup
submodule.subtypeLandcontinuous_linear_map.subtype_val(#15700)- committed
- committed
feat(analysis/normed_space/compact_operator): definition and basic facts about compact operators (#15467)
refactor(linear_algebra, analysis/inner_product_space): use
⊤ ≤instead of= ⊤in bases constructors (#15697)feat(linear_algebra/clifford_algebra/even): Universal property and isomorphisms for the even subalgebra (#14790)
feat(data/nat/factorization/basic): golf & move
card_multiples, prove variant lemmaIoc_filter_dvd_card_eq_div(#15277)feat(algebra/direct_sum/decomposition): add an induction principle for
direct_sum.decompositionclass (#15654)feat(field_theory/intermediate_field): Produce an intermediate field from a subalgebra satisfying
is_field. (#15659)
Commits on Aug 2, 2022
Commits on Sep 22, 2022
Commits on Sep 23, 2022
- committed
- committed
- committed
- committed
- committed