Skip to content
Permalink
Branch: master
Commits on Apr 11, 2019
  1. refactor(data/int/basic): weaken hypotheses for int.induction_on (#887)

    ChrisHughes24 authored and mergify committed Apr 11, 2019
    * refactor(data/int/basic): weaken hypotheses for int.induction_on
    
    * fix build
    
    * fix build
  2. feat(submonoid, subgroup, subring): is_ring_hom instances for set.inc…

    ChrisHughes24 authored and mergify committed Apr 11, 2019
    …lusion (#917)
Commits on Apr 10, 2019
  1. fix(mergify): merge if either push or pr build passes. (#918)

    ChrisHughes24 committed Apr 10, 2019
    * fix(mergify): merge if either push or pr build passes.
    
    * Update .mergify.yml
    
    * Update .mergify.yml
  2. feat(data/set/basic): inclusion map (#906)

    ChrisHughes24 authored and mergify committed Apr 10, 2019
    * feat(data/set/basic): inclusion map
    
    * add continuous_inclusion
    
    * minor style change
Commits on Apr 9, 2019
  1. feat(field_theory/subfield): subfields are fields (#888)

    ChrisHughes24 authored and mergify committed Apr 9, 2019
    * feat(field_theory/subfield): subfield are fields
    
    * Update subfield.lean
  2. fix(mergify): require travis "push" check to push (#913)

    ChrisHughes24 authored and cipher1024 committed Apr 9, 2019
    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
Commits on Apr 8, 2019
  1. feat(group_theory/subgroup): subtype.add_comm_group (#903)

    ChrisHughes24 committed Apr 8, 2019
  2. feat(analysis/complex/polynomial): fundamental theorem of algebra (#851)

    ChrisHughes24 authored and mergify committed Apr 8, 2019
    * 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
Commits on Apr 7, 2019
  1. feat(subgroup, subring, subfield): directed Unions of subrings are su…

    ChrisHughes24 authored and mergify committed Apr 7, 2019
    …brings (#889)
  2. feat(field_theory/subfield): is_subfield instances (#891)

    ChrisHughes24 committed Apr 7, 2019
Commits on Apr 6, 2019
Commits on Apr 3, 2019
  1. fix(README): fix mergify icon

    ChrisHughes24 committed Apr 3, 2019
Commits on Mar 31, 2019
  1. feat(data/polynomial): eval₂_neg

    ChrisHughes24 committed Mar 31, 2019
Commits on Mar 29, 2019
Commits on Mar 26, 2019
  1. feat(data/polynomial): rec_on_horner (#739)

    ChrisHughes24 authored and robertylewis committed Mar 26, 2019
Commits on Mar 22, 2019
Commits on Mar 16, 2019
  1. feat(group_theory/perm/cycles): cycle_factors (#815)

    ChrisHughes24 authored and avigad committed Mar 16, 2019
Commits on Mar 8, 2019
  1. refactot(data/equiv/basic): rename apply_inverse_apply to apply_symm_…

    ChrisHughes24 authored and robertylewis committed Mar 8, 2019
    …apply (#800)
Commits on Mar 7, 2019
  1. refactor(localization): shorten proofs (#796)

    ChrisHughes24 authored and robertylewis committed Mar 7, 2019
    * feat(algebra/group): units.coe_map
    
    * refactor(localization): shorten proofs
    
    *  swap order of equality in ring_equiv.symm_to_equiv
Commits on Mar 6, 2019
  1. feat(algebra/group): units.coe_map

    ChrisHughes24 committed Mar 6, 2019
Commits on Mar 2, 2019
  1. hopefully fixed for good this time

    ChrisHughes24 authored and avigad committed Mar 2, 2019
  2. fix properly

    ChrisHughes24 authored and avigad committed Mar 2, 2019
  3. fix build

    ChrisHughes24 authored and avigad committed Mar 2, 2019
  4. fix build

    ChrisHughes24 authored and avigad committed Mar 2, 2019
  5. generalize norm to zsqrtd

    ChrisHughes24 authored and avigad committed Mar 2, 2019
  6. fix build

    ChrisHughes24 authored and avigad committed Mar 2, 2019
  7. changing names

    ChrisHughes24 authored and avigad committed Mar 2, 2019
  8. The year is 2019

    ChrisHughes24 authored and avigad committed Mar 1, 2019
  9. move lemmas to correct places

    ChrisHughes24 authored and avigad committed Feb 28, 2019
  10. fix build

    ChrisHughes24 authored and avigad committed Feb 28, 2019
  11. finish proof of sum two squares

    ChrisHughes24 authored and avigad committed Feb 28, 2019
  12. commit properly

    ChrisHughes24 authored and avigad committed Feb 27, 2019
  13. prove Z[i] is a euclidean_domain

    ChrisHughes24 authored and avigad committed Feb 27, 2019
Commits on Mar 1, 2019
  1. feat(data/zmod/basic): cast_mod_nat' and cast_mod_int' (#783)

    ChrisHughes24 committed Mar 1, 2019
    * cast_mod_int'
    
    * cast_val_int'
Older
You can’t perform that action at this time.