feat(submonoid, subgroup, subring): is_ring_hom instances for set.inclusion #917
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
jcommelin
approved these changes
Apr 10, 2019
ChrisHughes24
added
the
ready-to-merge
amswerdlow
added a commit
that referenced
this pull request
May 30, 2019
* feat(algebra/field_power): add fpow_one, one_fpow, fpow_mul, mul_fpow (closes #855) * feat(scripts/cache_olean): cache and fetch olean binaries (#766) * script setup and documentation * fetch mathlib nightly when relevant * use credentials to access `github.com` * locate correct git directory, and add prompt * add confirmation message to setup-dev-scripts * adding --build-all option * refactor(*): unify group/monoid_action, make semimodule extend action (#850) * refactor(*): unify group/monoid_action, use standard names, make semimodule extend action * Rename action to mul_action * Generalize lemmas. Also, add class for multiplicative action on additive structure * Add pi-instances * Dirty hacky fix * Remove #print and set_option pp.all * clean up proof, avoid diamonds * Fix some build issues * Fix build * Rename mul_action_add to distrib_mul_action * Bump up the type class search depth in some places * feat(category_theory/instances): category of groups (#749) * fix(scripts/update-mathlib): update-mathlib shouldn't need github authentication * fix(scripts/update-mathlib): github authentication * fix(scripts/update-mathlib): fix imports of python files * feat(library_search): a simple library_search function (#839) * fix(scripts/deploy_nightly): pushing to the `lean-3.4.2` branch is sometimes blocked (#859) * fix(scripts/remote-install-update-mathlib): add GitPython dependency (#860) * feat(analysis/convex): convex sets and functions (#834) * refactor(data/zsqrtd/basic): move zsqrtd out of pell and into data (#861) * feat(data/polynomial): eval₂_neg * feat(data/complex/basic): smul_re,im * feat(data/finset): to_finset_eq_empty * feat(computability): computable_iff_re_compl_re * refactor(computability): unpack fixed_point proof * fix(ring_theory/algebra): remove duplicate theorems to fix build * feat(data/real/pi): Compute the first three digits of pi (#822) * fix(scripts/cache-olean): only run the post-checkout hook if we actually changed branches (#857) * refactor(analysis/convex): make instance local (#869) * docs(tactics): minor rewrite of exactI, resetI etc I always found these tactics confusing, but I finally figured out what they do and so I rewrote the docs so that I understand them better. * docs(tactics): add introduction to the instance cache tactic section * add tutorial about zmod37 (#767) Reference to a mathlib file which no longer exists has been fixed, and a more user-friendly example of an equivalence relation has been added in a tutorial. * feat(category_theory): working in Sort rather than Type (#824) * fix(build): prevent leanchecker from timing out * feat(tactic/push_neg): a tactic pushing negations (#853) * fix(tactic/congr'): some `\iff` goals were erroneously rejected * feat(data/nat/basic): nat.le_rec_on (#585) * fix(build): improve compatibility of caching scripts with Sourcetree (#863) * Inductive limit of metric spaces (#732) * fix(scripts/update-mathlib): protect file operations from interrupts (#864) * feat(tactic/local_cache): add tactic-block-local caching mechanism (#837) * build(travis): interrupt the build at the first error message (#708) Also make travis_long.sh print its progress messages to stderr. This sidesteps a mysterious issue where piping the output of travis_long.sh to another program caused that output to be lost (probably buffered somewhere?) so Travis would kill the build after 10 minutes. * chore(.travis.yml): use Lean to determine the Lean version (#714) * fix(int/basic): change order of instances to int.cast (#877) As discussed at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Problem.20with.20type.20class.20search/near/161848744 Changing the order of arguments lets type class inference fail quickly for `int -> nat` coercions, rather than repeatedly looking for `has_neg` on `nat`. * feat(tactic/basic): add `tactic.get_goal` (#876) * feat(algebra/pointwise): pointwise addition and multiplication of sets (#854) * feat(topology/uniform_space/pi): indexed products of uniform spaces (#845) * feat(topology/uniform_space/pi): indexed products of uniform spaces * fix(topology/uniform_space/pi): defeq topology * fix(src/topology/uniform_space/pi): typo Co-Authored-By: PatrickMassot <patrickmassot@free.fr> * feat(topology/metric_space/completion): completion of metric spaces (#743) * feat(ring_theory/algebra_operations): submodules form a semiring (#856) * feat(data/fin): add `fin.clamp` (#874) * chore(github/pr): mergify configuration (#871) * fix(README): fix mergify icon * chore(mergify): disable `delete_head_branch` * chore(mergify): use team names instead of user names * chore(mergify): fix config file * chore(mergify): fix config * fix(build): fix Lean version * feat (analysis/normed_space/basic.lean): implement reverse triangle inequality (#831) * implement reverse triangle inequality * make parameters explicit * feat(data/list/perm): nil_subperm (#882) * chore(github/pr): enable code owners * feat(algebra/char_p,field_theory/finite_card): cardinality of finite fields (#819) * First lemma's added * fixed lemmas by switching arguments * vector_space card_fin * char p implies zmod p module * Finite field card * renaming * . * bug fix * move to_module to is_ring_hom.to_module * fix bug * remove unnecessary open * instance instead of thm and remove unnecessary variables * moved cast_is_ring_hom and zmod.to_module to char_p * removed redundent nat.prime * some char_p stuff inside namespace char_p * fix * Moved finite field card to a different file * Removed unnecessary import * Remove unnecessary lemmas * Update src/algebra/char_p.lean Co-Authored-By: CPutz <casper.putz@gmail.com> * rename char_p lemmas * Minor changes * chore(mergify): delete head branch when merging * feat(category_theory): introduce the core of a category (#832) * feat(data/matrix): more basic matrix lemmas (#873) * feat(data/matrix): more basic matrix lemmas * feat(data/matrix): transpose_add * feat(data/list/min_max): minimum and maximum over list (#884) * feat(data/list/min_max): minimum and maximum over list * Update min_max.lean * replace semicolons * feat(list.split_on): [1,1,2,3,2,4,4].split_on 2 = [[1,1],[3],[4,4]] (#866) * feat(data/mllist): monadic lazy lists (#865) * feat(data/mllist): monadic lazy lists * oops, fix header * shove into tactic namespace * make mllist into a monad (#880) * make mllist into a monad * looks good. add `take`, and some tests * update authors * cleanup test * fix(scripts): not all files were deployed through the curl command * fix(scripts): Mac Python's test support doesn't work on Travis * fix(scripts): protect `leanpkg test` against timeouts * fix(build): match build names * feat(algebra/opposites): opposites of operators (#538) * more general hypotheses for integer induction (#885) * feat(category_theory/bifunctor): simp lemmas (#867) * feat(category_theory/bifunctor): simp lemmas * remove need for @, thanks Kenny and Chris! * fix(scripts): not all files were deployed through the curl command (#879) * chore(mergify): require the AppVeyor build to succeed * refactor(analysis/normed_space/bounded_linear_maps): nondiscrete normed field * fix(appveyor): build every commit * refactor(analysis/normed_space/bounded_linear_maps): nondiscrete normed field * fix(analysis/normed_space/bounded_linear_maps): fix build (#895) * fix(build): external PRs can't use GitHub credentials * feat(data/nat/basic): b = c if b - a = c - a (#862) * feat(field_theory/subfield): is_subfield instances (#891) * feat(subgroup, subring, subfield): directed Unions of subrings are subrings (#889) * feat(data/list/min_max): add minimum (#892) * fix(category_theory): turn `has_limits` classes into structures (#896) * fix(category_theory): turn `has_limits` classes into structures * fixing all the other pi-type typclasses * oops * trying to work out what was wrong with catching signals (#898) * feat(topology/gromov_hausdorff): the Gromov-Hausdorff space (#883) * feat(analysis/complex/polynomial): fundamental theorem of algebra (#851) * feat(data/complex/polynomia): fundamental theorem of algebra * fix build * add docstring * add comment giving link to proof used. * spag * move to analysis/complex * fix data/real/pi * Update src/analysis/complex/polynomial.lean Co-Authored-By: ChrisHughes24 <33847686+ChrisHughes24@users.noreply.github.com> * make Reid's suggested changes * make Reid's suggested changes * feat(linear_algebra/dual): add dual vector spaces (#881) * feat(linear_algebra/dual): add dual vector spaces Define dual modules and vector spaces and prove the basic theorems: the dual basis isomorphism and evaluation isomorphism in the finite dimensional case, and the corresponding (injectivity) statements in the general case. A variant of `linear_map.ker_eq_bot` and the "inverse" of `is_basis.repr_total` are included. Universe issues make an adaptation of `linear_equiv.dim_eq` necessary. * style(linear_algebra/dual): adapt to remarks from PR dsicussion * style(linear_algebra/dual): reformat proof of `ker_eq_bot'` * fix(doc/extra/tactic_writing): rename mul_left (#902) [ci skip] * fix(doc/extra/tactic_writing): rename mul_left * one more fix * feat(category_theory/colimits): missing simp lemmas (#894) * feat(group_theory/subgroup): subtype.add_comm_group (#903) * feat(order/lexicographic): lexicographic pre/partial/linear orders (#820) * remove prod.(*)order instances * feat(order/lexicographic): lexicographic pre/partial/linear orders * add lex_decidable_linear_order * identical constructions for dependent pairs * cleaning up * Update lexicographic.lean forgotten `instance` * restore product instances, and add lex type synonym for lexicographic instances * proofs in progress * * define lt * prove lt_iff_le_not_le * refactoring * refactor(*): rename is_group_hom.mul to map_mul (#911) * refactor(*): rename is_group_hom.mul to map_mul * Fix splits_mul * fix(mergify): require travis "push" check to push (#913) This hopefully fixes an error where mergify does not merge a PR is the "pr" build succeeds before the "push" build. In these situations mergify does not merge, because the branch protection settings require both builds to pass. Unfortunately, there doesn't seem to be an option to change the branch protection settings to only require the "pr" build to pass * chore(build): allow PRs from separate repos to test deployment scripts * feat(field_theory/subfield): subfields are fields (#888) * feat(field_theory/subfield): subfield are fields * Update subfield.lean * reorganising category_theory/instances/rings.lean (#909) * refactor(category_theory): rename `functor.on_iso` to `functor.map_iso` (#893) * feat(category_theory): functor.map_nat_iso * define `functor.map_nat_iso`, and relate to whiskering * rename `functor.on_iso` to `functor.map_iso` * add some missing lemmas about whiskering * some more missing whiskering lemmas, while we're at it * removing map_nat_iso * feat(data/set/basic): inclusion map (#906) * feat(data/set/basic): inclusion map * add continuous_inclusion * minor style change * refactor(algebra/group): is_monoid_hom extends is_mul_hom (#915) * refactor(algebra/group): is_monoid_hom extends is_mul_hom * Fix build * feat(category_theory): iso_whisker_(left|right) (#908) * feat(category_theory): iso_whisker_(left|right) * oops, use old notation for now * update after merge * fix(category_theory): make the `nat_trans` arrow `⟹` a synonym for the `hom` arrow (#907) * removing the nat_trans and vcomp notations; use \hom and \gg * a simpler proposal * getting rid of vcomp * fix * update notations in documentation * typo in docs * refactor(order/lexicographic): use prod.lex and psigma.lex (#914) * refactor(order/lexicographic): use prod.lex and psigma.lex * update * fix(mergify): merge if either push or pr build passes. (#918) * fix(mergify): merge if either push or pr build passes. * Update .mergify.yml * Update .mergify.yml * rename has_sum and is_sum to summable and has_sum (#912) * feat(analysis/normed_space/deriv): show that the differential is unique (2) (#916) * Remove wrong simp attribute * fix typo * characterize convergence at_top in normed spaces * copy some changes from #829 * small elements in normed fields go to zero * derivatives are unique * remove unnecessary lemma * update according to review * remove another empty line * minor changes (#921) * fix(tactic/explode): more accurate may_be_proof (#924) * feat(submonoid, subgroup, subring): is_ring_hom instances for set.inclusion (#917) * refactor(data/int/basic): weaken hypotheses for int.induction_on (#887) * refactor(data/int/basic): weaken hypotheses for int.induction_on * fix build * fix build * feat(algebra/free): free magma, semigroup, monoid (#735) * fix(algebra.field): introduce division_ring_has_div' (#852) * fix division_ring_has_div * priority default * comment * docs(elan): remove reference to nightly Lean (#928) * docs(elan): Remove reference to nightly Lean. * fix(algebra/big_operators): change variables in finset.prod_map to remove spurious [comm_monoid β] (#934) The old version involved maps α → β → γ and an instance [comm_monoid γ], but there was also a section variable [comm_monoid β]. In applications of this lemma it is not necessary, and not usually true, that β is a monoid. Change the statement to involve maps α → γ → β so that we already have a monoid structure on the last variable and we do not make spurious assumptions about the second one. * feat(scripts): disable testing the install scripts in external PRs (#936) * feat(topology/algebra/continuous_functions): the ring of continuous functions (#923) * feat(topology/algebra/continuous_functions): the ring of continuous functions * filling in the hierarchy * use to_additive * feat(nat/basic): add some basic nat inequality lemmas (#937) * feat(nat/basic): add some basic nat inequality lemmas, useful as specific cases of existing ring cases since uses less hypothesis * feat(nat/basic): add some basic nat inequality lemmas, with convention fixes * feat(nat/basic): add some basic nat inequality lemmas, with convention fixes * feature(category_theory/instances/Top/open[_nhds]): category of open sets, and open neighbourhoods of a point (merge #920 first) (#922) * rearrange Top * oops, import from the future * the categories of open sets and of open_nhds * missing import * restoring opens, adding headers * Update src/category_theory/instances/Top/open_nhds.lean Co-Authored-By: semorrison <scott@tqft.net> * use full_subcategory_inclusion * feat(data/set/intervals): some interval lemmas (#942) * feat(data/set/intervals): a few more lemmas * one-liners * feat(data/finset): powerset_len (subsets of a given size) (#899) * feat(data/finset): powerset_len (subsets of a given size) * fix build * feat(*): various additions to low-level files (#904) * feat(*): various additions to low-level files * fix(data/fin): add missing universe * fix(test/local_cache): make the trace text explicit and quiet (#941) (by default) * feat(tactic/omega): tactic for linear integer & natural number arithmetic (#827) * feat(tactic/omega): tactic for discharging linear integer and natural number arithmetic goals * refactor(tactic/omega): clean up namespace and notations * Update src/data/list/func.lean Co-Authored-By: skbaek <seulkeebaek@gmail.com> * Add changed files * Refactor val_between_map_div * Use default inhabitants for list.func * feat(scripts): use apt-get on ubuntu and support older Python versions (#945) * feat(analysis/normed_space): more facts about operator norm (#927) * refactor(analysis/normed_space): refactor and additional lemmas - rename `bounded_linear_maps` to `bounded_linear_map`, `operator_norm` to `op_norm`. - refactor operator norm with an equivalent definition. - change some names and notation to be more consistent with conventions elsewhere in mathlib: replace `bounded_by_*` with `le_*`, `operator_norm_homogeneous` with `op_norm_smul`. - more simp lemmas for bounded_linear_map. - additional results: lipschitz continuity of the operator norm, also that it is submultiplicative. * chore(analysis/normed_space/operator_norm): add attribution * style(analysis/normed_space/operator_norm): use namespace `real` - open `real` instead of `lattice` and omit spurious prefixes. * feat(analysis/normed_space/operator_norm): coercion to linear_map * style(analysis/normed_space/bounded_linear_maps): minor edits - extract variables for brevity of theorem statements. - more consistent naming of variables. * feat(analysis/normed_space/operator_norm): add constructor of bounded_linear_map from is_bounded_linear_map * fix(analysis/normed_space/operator_norm): remove spurious explicit argument * fix(analysis/normed_space): type of bounded linear maps - change the definition of bounded_linear_map to be a type rather than the corresponding subspace, and mark it for unfolding. - rename `bounded_linear_map.from_is_bounded_linear_map` to `is_bounded_linear_map.to_bounded_linear_map`. * feat(analysis/normed_space): analysis results for bounded_linear_maps * feat(group_theory/subgroup): additive version of inj_iff_trivial_ker (#947) * style(tactic/omega): whitespace and minor tweaks missed the PR review cycle * feat(tactic/ring): treat expr atoms up to defeq (#949) * fix(topology/order): Missing Prop annotation (#952) * feat(tactic/linarith): treat expr atoms up to defeq (#950) * feat(data/[fin]set): add some more basic properties of (finite) sets (#948) * feat(data/[fin]set): add some more basic properties of (finite) sets * update after reviews * fix error, move pairwise_disjoint to lattice as well * fix error * feat(tactic/clear_except): clear most of the assumptions in context (#957) * fix(tactic/interactive): allow `convert e using 0` * feat(data/list/basic): index_of_inj (#954) * feat(data/list/basic): index_of_inj * make it an iff * refactor(data/equiv/basic): simplify definition of equiv.set.range (#959) * refactor(data/equiv/basic): simplify definition of equiv.set.range * delete duplicate * fix(ring_theory/adjoin_root): move adjoin_root out of adjoin_root namespace (#960) * feat(function/embedding): ext and ext_iff (#962) * refactor(analysis/normed_space/operator_norm): replace subspace with … (#955) * refactor(analysis/normed_space/operator_norm): replace subspace with structure * refactor(analysis/normed_space/operator_norm): add coercions * feat(data/equiv/basic): sum_compl_apply and others (#961) * feat(data/equiv/basic): sum_congr_apply and others * Update basic.lean * fix(README): update maintainer list * refactor(analysis/normed_space): use bundled type for `fderiv` (#956) * feat(analysis/normed_space): refactor fderiv to use bounded_linear_map - uniqueness remains sorry'd - more simp lemmas about bounded_linear_map * refactor uniqueness proof * fix(analysis/normed_space/operator_norm): rename `bound_le_op_norm` to `op_norm_le_bound` - so that the inequality goes the correct way. * Update elan.md * refactor(tactic/interactive): remove dependencies of (#878) `tactic/interactive` on many theories * feat(analysis/normed_space): open mapping (#900) * The Banach open mapping theorem * improve comments * feat(analysis/normed_space): rebase, fix build * fix(scripts/remote-install-update-mathlib): missing dependency (#964) Also add a `--upgrade` option to `pip install` in case something is already there but outdated * fix(scripts/remote-install-update-mathlib): try again [ci skip] The previous attempt to install setuptools seems to fails for timing reasons (PyGithub need setuptools after it's downloaded but before it is installed, this is probably also a packaging issue in PyGithub). * chore(category_theory): move small_category_of_preorder to preorder namespace (#932) * feat(script/auth_github): improve messages [ci skip] (#965) * feat(category_theory/limits): complete lattices have (co)limits (#931) * feat(category_theory/limits): complete lattices have (co)limits * Update lattice.lean * fix(tactic/library_search): iff lemmas with universes (#935) * fix(tactic/library_search): iff lemmas with universes * cleaning up * add crossreference * feat(category_theory/limits/opposites): (co)limits in opposite categories (#926) * (co)limits in opposite categories * moving lemmas * moving stuff about complete lattices to separate PR * renaming category_of_preorder elsewhere * build limits functor/shape at a time * removing stray commas, and making one-liners * remove non-terminal simps * feat(ring_theory/ideal_operations): inj_iff_trivial_ker for ring homomorphisms (#951) * feat(ring_theory/ideal_operations): inj_iff_trivial_ker for ring homomorphisms * Update subgroup.lean * Update ideal_operations.lean * fix(script/remote-install-update-mathlib) fix answer reading and requests/urllib3 version conflict (#968) * fix(scripts/remote-install-update-mathlib): apt shouldn't ask (#969) * fix(data/polynomial): change instance order in polynomial.subsingleton (#970) * remove code duplication (#971) * chore(docs): delete docs/wip.md (#972) * chore(docs): delete docs/wip.md long outdated * remove link in README * chore(travis): disable the check for minimal imports (#973) * feat(category_theory/limits): support for special shapes of (co)limits (#938) feat(category_theory/limits): support for special shapes of (co)limits * feat(docs/install_debian): Debian startup guide (#974) * feat(docs/install_debian): Debian startup guide * feat(scripts/install_debian): One-line install for Debian [ci skip] * fix(docs/install_debian*): Typos pointed out by Johan Also adds a summary of what will be installed * chore(README): put the badges in the README on one line (#975) * chore(build): build only master and its related PRs * feat(tactic/decl_mk_const): performance improvement for library_search (#967) * feat(tactic/decl_mk_const): auxiliary tactic for library_search [WIP] * use decl_mk_const in library_search * use decl_mk_const * move into tactic/basic.lean * feat(option/injective_map) (#978) * feat(colimits): arbitrary colimits in Mon and CommRing (#910) * feat(category_theory): working in Sort rather than Type, as far as possible * missed one * adding a comment about working in Type * remove imax * removing `props`, it's covered by `types`. * fixing comment on `rel` * tweak comment * add matching extend_π lemma * remove unnecessary universe annotation * another missing s/Type/Sort/ * feat(category_theory/shapes): basic shapes of cones and conversions minor tweaks * Moving into src. Everything is borked. * investigating sparse * blech * maybe working again? * removing terrible square/cosquare names * returning to filtered colimits * colimits in Mon * rename * actually jump through the final hoop * experiments * fixing use of ext * feat(colimits): colimits in Mon and CommRing * fixes * removing stuff I didn't mean to have in here * minor * fixes * merge * update after merge * fix import * feat(logic/basic): forall_iff_forall_surj (#977) a lemma from the perfectoid project * fix(data/set/finite): make fintype_seq an instance (#979) * feat(data/set/basic): prod_subset_iff (#980) * feat(data/set/basic): prod_subset_iff * syntax * feat(presheaves) (#886) * feat(category_theory/colimits): missing simp lemmas * feat(category_theory): functor.map_nat_iso * define `functor.map_nat_iso`, and relate to whiskering * rename `functor.on_iso` to `functor.map_iso` * add some missing lemmas about whiskering * fix(category_theory): presheaves, unbundled and bundled, and pushforwards * restoring `(opens X)ᵒᵖ` * various changes from working on stalks * rename `nbhds` to `open_nhds` * fix introduced typo * typo * compactify a proof * rename `presheaf` to `presheaf_on_space` * fix(category_theory): turn `has_limits` classes into structures * naming instances to avoid collisions * breaking up instances.topological_spaces * fixing all the other pi-type typclasses * fix import * oops * fix import * missed one * typo * restoring eq_to_hom simp lemmas * removing unnecessary simp lemma * remove another superfluous lemma * removing the nat_trans and vcomp notations; use \hom and \gg * a simpler proposal * getting rid of vcomp * fix * splitting files * update notation * fix * cleanup * use iso_whisker_right instead of map_nat_iso * proofs magically got easier? * improve some proofs * remove crap * minimise imports * chore(travis): disable the check for minimal imports * Update src/algebraic_geometry/presheafed_space.lean Co-Authored-By: semorrison <scott@tqft.net> * writing `op_induction` tactic, and improving proofs * squeeze_simping * cleanup * rearranging * Update src/category_theory/instances/Top/presheaf.lean Co-Authored-By: semorrison <scott@tqft.net> * fix `open` statements, and use `op_induction` * rename terms of PresheafedSpace to X Y Z. rename field from .X to .to_Top * forgetful functor * update comments about unfortunate proofs * add coercion from morphisms of PresheafedSpaces to morphisms in Top * feat(category_theory/products): associators (#982) * feat(ring_theory/adjoin): adjoining elements to form subalgebras (#756) * feat(ring_theory/adjoin): adjoining elements to form subalgebras * Fix build * Change to_submodule into a coercion * Use pointwise_mul * add simp attribute to adjoin_empty * six(style.md): fix broken code (#987) * feat(category_theory): currying for functors (#981) * feat(category_theory): currying for functors * Update src/category_theory/currying.lean Co-Authored-By: semorrison <scott@tqft.net> * compacting * fix import * change from review * rfl on same line * chore(build): build against Lean 3.5 nightly build (#989) * chore(build): fix stages in cron job * feat(category/monad/cont): monad_cont instances for state_t, reader_t, except_t and option_t (#733) * feat(category/monad/cont): monad_cont instances for state_t, reader_t, except_t and option_t * feat(category/monad/writer): writer monad transformer * chore(build): cron build restarts from scratch * feat(scripts): add --build-new flag to cache-olean (#992) * building the hyperreal library (#835) * more instances * fix stuff that got weirded * fix stuff that got weird * fix stuff that became weird * build hyperreal library (with sorries) * fix weirdness, prettify etc. * spaces * st lt le lemmas fix type * Update src/data/real/hyperreal.lean Co-Authored-By: abhimanyupallavisudhir <43954672+abhimanyupallavisudhir@users.noreply.github.com> * if then * more stuff * Update hyperreal.lean * Update hyperreal.lean * Update basic.lean * Update basic.lean * Update hyperreal.lean * of_max, of_min, of_abs * Update filter_product.lean * Update hyperreal.lean * abs_def etc. * Update filter_product.lean * hole * Update hyperreal.lean * Update filter_product.lean * Update filter_product.lean * Update filter_product.lean * Update hyperreal.lean * Update hyperreal.lean * Update filter_product.lean * Update hyperreal.lean * Update hyperreal.lean * finally done with all sorries! * Update hyperreal.lean * fix (?) * fix (?) ring issue * real.Sup_univ * st is Sup * st_id_real spacebar * sup --> Sup * fix weirds * dollar signs * 100-column * 100 columns rule * Update hyperreal.lean * removing uparrows * uparrows * some stuff that got away * fix * lift_id * fix? * fix mono, hopefully * fix mono, hopefully * this should work * fix -- no more mono * fixes * fixes * fixes * fixes * ok, fixed * feat(category_theory/category_of_elements) (#990) * feat(category_theory/category_of_elements) * Update src/category_theory/elements.lean Co-Authored-By: semorrison <scott@tqft.net> * Update src/category_theory/elements.lean Co-Authored-By: semorrison <scott@tqft.net> * Update src/category_theory/elements.lean Co-Authored-By: semorrison <scott@tqft.net> * Update src/category_theory/punit.lean Co-Authored-By: semorrison <scott@tqft.net> * various * remaining simp lemmas * feat(group_theory/subgroup): is_subgroup.inter (#994) * chore(tactics): splitting tactics and tests into more files (#985) * chore(tactics): splitting tactics and tests into more files, cleaning up dependencies * tweaking comment * introducing `tactic.basic` and fixing imports * fixes * fix copyright * fix some things * feat(*): preorder instances for with_bot and with_zero (#996) * feat(*): preorder instances for with_bot and with_zero * Let's try again * refactor(order/basic): make type class args explicit in {*}order.lift (#995) * refactor(order/basic): make type class arguments explicit for {*}order.lift * Let's try again * And another try * Silly typo * Fix error * Oops, missed this one * refactor(strict_mono): make definition + move to order_functions (#998) * refactor(strict_mono): make definition + move to order_functions * Weaken assumptions from preorder to has_lt * feat(algebra/pointwise): More lemmas on pointwise multiplication (#997) * feat(algebra/pointwise): More lemmas on pointwise multiplication * Fix build, hopefully * Fix build * to_additive + fix formatting * feat(set_theory): add to cardinal, ordinal, cofinality (#963) * feat(set_theory): add to cardinal, ordinal, cofinality The main new fact is the infinite pigeonhole principle Also includes many basic additions * fix name change in other files * address all of Mario's comments * use classical tactic in order/basic I did not use it for well_founded.succ, because that resulted in an error in lt_succ * fix error * fix(tactic/basic): missing `conv` from tactic.basic (#1004) * fix(category/fold): use correct `opposite` (#1008) * refactor(algebra/associated): rename nonzero_of_irreducible to ne_zero_of_irreducible (#1009) * feat(data/polynomial): degree_eq_one_of_irreducible_of_root (#1010) * chore(compatibility): compatibility with Lean 3.5.0c (#1007) * docs(algebra/ring): document compatibility hack [skip ci] * chore(build): remove script testing on PRs [skip ci] * fix(docs/*): docs reorganization [skip ci] (#1012) * feat(logic/function): comp₂ -- useful for binary operations (#993) * feat(logic/function): comp₂ -- useful for binary operations For example, when working with topological groups it does not suffice to look at `mul : G → G → G`; we need to require that `G × G → G` is continuous. This lemma helps with rewriting back and forth between the curried and the uncurried versions. * Fix: we are already in the function namespace, duh * Replace comp₂ with a generalisation of bicompr * fix error in bitraversable * partially open function namespace in bitraversable * feat(topology/maps): closed embeddings (#1013) * feat(topology/maps): closed embeddings * fix "is_open_map" * feat(category_theory): lemmas about cancellation (#1005) * feat(category_theory): lemmas about cancellation * rename hypotheses * Squeeze proofs * chore(scripts): migrate scripts to own repo (#1011) * chore(Github): no need to wait for Appveyor anymopre * feat(Top.presheaf_ℂ): presheaves of functions to topological commutative rings (#976) * feat(category_theory/colimits): missing simp lemmas * feat(category_theory): functor.map_nat_iso * define `functor.map_nat_iso`, and relate to whiskering * rename `functor.on_iso` to `functor.map_iso` * add some missing lemmas about whiskering * fix(category_theory): presheaves, unbundled and bundled, and pushforwards * restoring `(opens X)ᵒᵖ` * various changes from working on stalks * rename `nbhds` to `open_nhds` * fix introduced typo * typo * compactify a proof * rename `presheaf` to `presheaf_on_space` * fix(category_theory): turn `has_limits` classes into structures * naming instances to avoid collisions * breaking up instances.topological_spaces * fixing all the other pi-type typclasses * fix import * oops * fix import * missed one * typo * WIP * oops * the presheaf of continuous functions to ℂ * restoring eq_to_hom simp lemmas * removing unnecessary simp lemma * remove another superfluous lemma * removing the nat_trans and vcomp notations; use \hom and \gg * a simpler proposal * getting rid of vcomp * fix * splitting files * renaming * update notation * fix * cleanup * use iso_whisker_right instead of map_nat_iso * proofs magically got easier? * improve some proofs * moving instances * remove crap * tidy * minimise imports * chore(travis): disable the check for minimal imports * Update src/algebraic_geometry/presheafed_space.lean Co-Authored-By: semorrison <scott@tqft.net> * writing `op_induction` tactic, and improving proofs * squeeze_simping * cleanup * rearranging * cleanup * cleaning up * cleaning up * move * Update src/category_theory/instances/Top/presheaf_of_functions.lean Co-Authored-By: Floris van Doorn <fpvdoorn@gmail.com> * fixes in response to review * document the change in scripts (#1024) * feat(category_theory/iso): missing lemmas (#1001) * feat(category_theory/iso): missing lemmas * formatting * formatting * oops * one more * sleep * feat(category_theory/products): missing simp lemmas (#1003) * feat(category_theory/products): missing simp lemmas * cleanup proofs * fix proof * squeeze_simp * feat(tactics/interactive): choose uses exists_prop (#1014) * feat(tactics/interactive): choose uses exists_prop * fix build * feat(data/equiv/basic): equiv.nonempty_iff_nonempty (#1020) * feat(topology/constructions): topology of sum types (#1016) * feat(algebra/order_functions): generalize strict_mono.monotone (#1022) * feat(category_theory/opposites): iso.op (#1021) * squeeze_simp (#1019) * feat(analysis/normed_space/deriv): more material on derivatives (#966) * feat(analysis/normed_space/deriv): more material on derivatives * feat(analysis/normed_space/deriv): minor improvements * feat(analysis/normed_space/deriv) rename fderiv_at_within to fderiv_within_at * feat(analysis/normed_space/deriv): more systematic renaming * feat(analysis/normed_space/deriv): fix style * modify travis.yml as advised by Simon Hudon * fix travis.yml, second try * feat(analysis/normed_space/deriv): add two missing lemmas * fix(data/multiset): remove duplicate setoid instance (#1027) * fix(data/multiset): remove duplicate setoid instance * s/ : Type uu// * feat(tactic): new tactics to normalize casts inside expressions (#988) * new tactics for normalizing casts * update using the norm_cast tactics * minor proof update * minor changes * moved a norm_cast lemma * minor changes * fix(doc/tactics): make headers uniform * nicer proof using discharger * fixed numerals handling by adding simp_cast lemmas * add documentation * fixed unnecessary normalizations in assumption_mod_cast * minor proof update * minor coding style update * documentation update * rename flip_equation to expr.flip_eq * update proofs to remove boiler plate code about casts * revert to old proof * fixed imports and moved attributes * add test file * new attribute system - the attribute norm_cast is split into norm_cast and norm_cast_rev - update of the equation flipping mechanism - update of the numerals handling * syntax fix * change attributes names * test update * small update * add elim_cast attribute * add examples for attributes * new examples * fix(docs/tactics): fix layout, remove noise * feat(data/equiv/functor): map_equiv (#1026) * feat(data/equiv/functor): map_equiv * golf proofs * feat(data/nat/basic): decreasing induction (#1031) * feat(data/nat/basic): decreasing induction * feat(data/nat/basic): better proof of decreasing induction * feat(category_theory): adjoint equivalences and limits under equivalences (#986) * feat(category_theory): adjoint equivalences and limits * Define equivalences to be adjoint equivalences. * Show that one triangle law implies the other for equivalences * Prove that having a limit of shape `J` is preserved under an equivalence `J ≌ J'`. * Construct an adjoint equivalence from a (non-adjoint) equivalence * Put `nat_iso.app` in the `iso` namespace, so that we can write `α.app` for `α : F ≅ G`. * Add some basic lemmas about equivalences, isomorphisms. * Move some lemmas from `nat_trans` to `functor_category` and state them using `F ⟶ G` instead of `nat_trans F G` (maybe these files should just be merged?) * Some small tweaks, improvements * opposite of discrete is discrete This also shows that C^op has coproducts if C has products and vice versa Also fix rebase errors * fix error (I don't know what caused this to break) * Use tidy a bit more * construct an adjunction from an equivalence add notation `⊣` for an adjunction. make some arguments of adjunction constructors implicit * use adjunction notation * formatting * do adjointify_η as a natural iso directly, to avoid checking naturality * tersifying * fix errors, a bit of cleanup * fix elements.lean * fix error, address comments * feat(tactic/terminal_goal): determine if other goals depend on the current one (#984) * feat(tactics): add "terminal_goal" tactic and relatives * fix(test/tactics): renaming test functions to avoid a name collision * fix(tactic): moving terminal_goal to tactic/basic.lean * fix(test/tactics): open tactics * touching a file, to prompt travis to try again * terminal_goal * fix * merge * refactor(topology): change continuous_at_within to continuous_within_at (#1034) * feat(category_theory): monos and epis in Type and Top (#1030) * feat(category_theory): monos and epis in Type and Top * imports * add file header * use notation for adjunction * chore(*): reduce imports (#1033) * chore(*): reduce imports * restoring import in later file * fix import * fix(data/nat/enat): Fix typo in lemma name (#1037) * feat(data/nat/basic): make decreasing induction eliminate to Sort (#1032) * add interface for decreasing_induction to Sort * make decreasing_induction a def * add simp tags and explicit type * chore(opposites): merge two definitions of `opposite` (#1036) * chore(opposites): merge two definitions of `opposite` * merge `opposite.opposite` from `algebra/opposites` with `category_theory.opposite` from `category_theory/opposites`, and put it into `data/opposite` * main reasons: DRY, avoid confusion if both namespaces are open * see #538 (comment) * Authors merged from `git blame` output on both original files; I assume my contribution to be trivial * Update opposite.lean * fix(data/complex/exponential): make complex.exp irreducible (#1040) See discussion at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/-T50000.20challenge Using `ring` (and other tactics) on terms involving `exp` can lead to some unpleasant and unnecessary unfolding. * feat(tactic/basic): add tactic.rewrite, and sort list (#1039) * refactor: change variables order in some composition lemmas (#1035) * feat(set_theory/surreal): surreal numbers (#958) * feat(set_theory/surreal): surreal numbers * doc(set_theory/surreal): surreal docs * minor changes in surreal * fix(topology/stone_cech): faster proof from @PatrickMassot (#1042) * feat(adjointify): make definition easier for elaborator (#1045) * refactor(data/complex/exponential): improve trig proofs (#1041) * fix(data/complex/exponential): make complex.exp irreducible See discussion at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/-T50000.20challenge Using `ring` (and other tactics) on terms involving `exp` can lead to some unpleasant and unnecessary unfolding. * refactor(data/complex/exponential): improve trig proofs * fix build * fix(algebra/group): prove lemma for comm_semigroup instead of comm_monoid * feat(tactic/squeeze): remove noise from output (#1047) * feat(topology/order): make nhds irreducible (#1043) * feat(topology/order): make nhds irreducible * move nhds irreducible to topology.basic * refactor(topology/metric/gromov_hausdorff): make Hausdorff_edist irreducible (#1052) * refactor(topology/metric/gromov_hausdorff): remove linarith calls * refactor(topology/metric/hausdorff_dist): make hausdorff_dist irreducible * refactor: coherent composition order (#1055) * feat(tactic/linarith): better input syntax linarith only [...] (#1056) * feat(tactic/ring, tactic/linarith): add reducibility parameter * fix(tactic/ring): interactive parsing for argument to ring1 * feat(tactic/linarith): better input syntax linarith only [...] * fix(docs/tactics): fix linarith doc * feat(topology/opens): continuous.comap : opens Y → opens X (#1061) * feat(topology/opens): continuous.comap : opens Y → opens X From the perfectoid project. * Update opens.lean * feat(tactic/basic): adds `contrapose` tactic (#1015) * feat(tactic/basic): adds `contrapose` tactic * fix(tactic/push_neg): fix is_prop testing * Setup error message testing following Rob, add tests for `contrapose` * refactor(tactic/interactive): move noninteractive success_if_fail_with_msg to tactic/core * chore(ring_theory/algebra): simp-lemmas for alg_hom.to_linear_map (#1062) * chore(ring_theory/algebra): simp-lemmas for alg_hom.to_linear_map From the perfectoid project. * Stupid error * Update src/ring_theory/algebra.lean Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com> * chore(topology/algebra/monoid): continuous_mul_left/right (#1065) * feat(category_theory): limits in CommRing (#1006) * feat(category_theory): limits in CommRing * by * rename * sections * Update src/category_theory/types.lean Co-Authored-By: Johannes Hölzl <johannes.hoelzl@gmx.de> * feat(algebra/pi_instances): product of submonoids/groups/rings (#1066) From the perfectoid project. * refactor(integration.lean): changing `measure_space` to `measurable_space` (#1072) I've been using this file and `range_const` doesn't seem to require the spurious `measure_space` instance. `measurable_space` seems to suffice. * feat(*): image_closure (#1069) Prove that the image of the closure is the closure of the image, for submonoids/groups/rings. From the perfectoid project. * feat(data/nat): various lemmas (#1017) * feat(data/nat): various lemmas * protect a definition * fixes * Rob's suggestions * Mario’s proof (Working offline, let’s see what Travis says) * minigolf * feat(linear_algebra/basic): general_linear_group basics (#1064) * feat(linear_algebra/basic): general_linear_group basics This patch proves that the general_linear_group (defined as units in the endomorphism ring) are equivalent to the group of linear equivalences. * shorten proof of ext * Add mul_equiv * Use coe * Fix stupid error * doc(finsupp,category_theory): fixes (#1075) * doc * update emb_domain doc string * typo * chore(CommRing/adjunctions): refactor proofs (#1049) * splitting adjunction.lean * chore(CommRing/adjunctions): refactor proofs * remove unnecessary assumptions * add helpful doc-string * cleanup * breaking things, haven't finished yet * deterministic timeout * unfold_coes to the rescue * one more int.cast * yet another int.cast * Update src/data/mv_polynomial.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * Update src/data/mv_polynomial.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * WIP * Fix build * Fix build * refactor(set_theory/ordinal): shorten proof of well_ordering_thm (#1078) * refactor(set_theory/ordinal): shorten proof of well_ordering_thm§ * Update ordinal.lean * Update ordinal.lean * Update ordinal.lean * Improve readability * shorten proof * Shorten proof * feat(group_theory/conjugates) : define conjugates (#1029) * feat(algebra/order_functions): generalize strict_mono.monotone (#1022) * moving stuff to where it belongs * removed unecessary import * Changed to union * Update src/group_theory/subgroup.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * Stylistic changes * Added authorship * Moved mem_conjugates_of_set * Authorship * Trying fixes * Putting everything in the right order * removed import * fix(tactic/rcases): add parse desc to rcases/rintro (#1091) * feat(ordered_group): add missing instance (#1094) * feat(presheaves/stalks): stalks of presheafs, and presheafed spaces with extra structure on stalks (#1018) * feat(category_theory/colimits): missing simp lemmas * feat(category_theory): functor.map_nat_iso * define `functor.map_nat_iso`, and relate to whiskering * rename `functor.on_iso` to `functor.map_iso` * add some missing lemmas about whiskering * fix(category_theory): presheaves, unbundled and bundled, and pushforwards * restoring `(opens X)ᵒᵖ` * various changes from working on stalks * rename `nbhds` to `open_nhds` * fix introduced typo * typo * compactify a proof * rename `presheaf` to `presheaf_on_space` * fix(category_theory): turn `has_limits` classes into structures * naming instances to avoid collisions * breaking up instances.topological_spaces * fixing all the other pi-type typclasses * fix import * oops * fix import * feat(category_theory): stalks of sheaves * renaming * fixes after rebase * nothing * yay, got rid of the @s * attempting a very general version of structured stalks * missed one * typo * WIP * oops * the presheaf of continuous functions to ℂ * restoring eq_to_hom simp lemmas * removing unnecessary simp lemma * remove another superfluous lemma * removing the nat_trans and vcomp notations; use \hom and \gg * a simpler proposal * getting rid of vcomp * fix * splitting files * renaming * probably working again? * update notation * remove old lemma * fix * comment out unfinished stuff * cleanup * use iso_whisker_right instead of map_nat_iso * proofs magically got easier? * improve some proofs * moving instances * remove crap * tidy * minimise imports * chore(travis): disable the check for minimal imports * Update src/algebraic_geometry/presheafed_space.lean Co-Authored-By: semorrison <scott@tqft.net> * writing `op_induction` tactic, and improving proofs * squeeze_simping * cleanup * rearranging * cleanup * cleaning up * cleaning up * move * cleaning up * structured stalks * comment * structured stalks * more simp lemmas * formatting * Update src/category_theory/instances/Top/presheaf_of_functions.lean Co-Authored-By: Floris van Doorn <fpvdoorn@gmail.com> * fixes in response to review * tidy regressions... :-( * oops * Update src/algebraic_geometry/presheafed_space.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * Update src/algebraic_geometry/presheafed_space.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * Update src/algebraic_geometry/presheafed_space.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * Update src/category_theory/instances/TopCommRing/basic.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * def to lemma * remove useless lemma * explicit associator * broken * can't get proofs to work... * remove superfluous imports * missing headers * change example * reverting changes to tidy * remove presheaf_Z, as it doesn't work at the moment * fixes * fixes * fix * postponing stuff on structured stalks for a later PR * coercions * getting rid of all the `erw` * omitting some proofs * deleting more proofs * convert begin ... end to by * local * feat(ring_theory): free_ring and free_comm_ring (#734) * feat(ring_theory): free_ring and free_comm_ring * Define isomorphism with mv_polynomial int * Ring hom free_ring -> free_comm_ring; 1 sorry left * Coe from free_ring to free_comm_ring is ring_hom * WIP * WIP * WIP * WIP * Refactoring a bunch of stuff * functor.map_equiv * Fix build * Fix build * Make multiset.subsingleton_equiv computable * Define specific equivs using general machinery * Fix build * Remove old commented code * feat(data/equiv/functor): map_equiv * fix(data/multiset): remove duplicate setoid instance * namespace changes * feat(category_theory/monoidal): monoidal categories, monoidal functors (#1002) * feat(category_theory/iso): missing lemmas * formatting * formatting * almost * oops * getting there * one more * sleep * good to go * fix names * renaming * linebreak * temporary notations * notations for associator, unitors? * more notation * names * more names * oops * renaming, and namespaces * comment * fix comment * remove unnecessary open, formatting * removing dsimps * replace with simp lemmas * fix
anrddh
pushed a commit
to anrddh/mathlib
that referenced
this pull request
May 15, 2020
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
TO CONTRIBUTORS:
Make sure you have:
If this PR is related to a discussion on Zulip, please include a link in the discussion.
For reviewers: code review check list