Commits leanprover-community/mathlib

Update algebra_map.lean

vihdzp committed 3 years ago

b5b4aa3e

feat(algebra/algebra/subalgebra/basic): Swap arguments of `map` and `comap` (#15744)

tb65536 committed 3 years ago

348a674b

refactor(tactic/lint/type_classes): change inhabited linter to nonempty linter (#15542)

kmill committed 3 years ago

14b69e9f

feat(algebra/big_operators): add lemmas about sum of disjoint multiset (#15556)

xroblot committed 3 years ago

20f97964

feat(group_theory/p_group): Groups of order p^2 are commutative (#8632)

ChrisHughes24 committed 3 years ago

09afe572

refactor(algebra/homology): better defeqs, less case splitting (#15690)

jcommelin committed 3 years ago

13ff898b

fix(linear_algebra/prod): add missing `of_dual`s in lemma statements (#15750)

eric-wieser committed 3 years ago

cb3c2b9e

feat(field_theory/adjoin): A compositum of algebraic extensions is algebraic (#15724)

tb65536 committed 3 years ago

daac51e8

feat(field_theory/intermediate_field): Produce an intermediate field from a subalgebra satisfying `is_field`. (#15659)

tb65536 committed 3 years ago

7afd66ab

feat(algebra/direct_sum/decomposition): add an induction principle for `direct_sum.decomposition` class (#15654)

jjaassoonn committed 3 years ago

725ad273

feat(data/finset/pointwise): Singleton arithmetic (#15435)

YaelDillies committed 3 years ago

0fc357f5

feat(data/nat/factorization/basic): golf & move `card_multiples`, prove variant lemma `Ioc_filter_dvd_card_eq_div` (#15277)

stuart-presnell committed 3 years ago

87861dd7

docs(measure_theory/measure/haar): Mention uniqueness in module docstring (#15740)

rwbarton committed 3 years ago

df203bc8

docs(topology/sets/compacts): fix typo (#15739)

rwbarton committed 3 years ago

b7bde9df

feat(linear_algebra/matrix): inner prod of matrix (#14794)

abentkamp committed 3 years ago

1d0df917

feat(linear_algebra/clifford_algebra/even): Universal property and isomorphisms for the even subalgebra (#14790)

eric-wieser committed 3 years ago

56199b7b

refactor(linear_algebra, analysis/inner_product_space): use `⊤ ≤` instead of `= ⊤` in bases constructors (#15697)

ADedecker committed 3 years ago

6b647c3b

feat(analysis/normed_space/compact_operator): definition and basic facts about compact operators (#15467)

ADedecker committed 3 years ago

4ff8c3db

feat(probability/strong_law): Lp version of the strong law of large numbers (#15392)

kex-y committed 3 years ago

b33d6d6e

fix(tactic/polyrith): remove unnecessary 1* from polyrith output (#15292)

robertylewis committed 3 years ago

5fc18b5e

feat(data/{pi, prod}): add missing `has_pow` instances for `pi` type (#15478)

jjaassoonn committed 3 years ago

39046bda

feat(algebra/module): sub_mem_sup for modules over rings (#15733)

alexjbest committed 3 years ago

8b87d337

feat(data/pi/algebra): sum_elim lemmas (#15588)

abentkamp committed 3 years ago

1065169f

feat(test/polyrith): better formatting for generated tests (#15728)

robertylewis committed 3 years ago

94dcadd5

chore(field_theory/splitting_field): remove unneeded parameter (#15716)

Vierkantor committed 3 years ago

123f4542

feat(group_theory/finite_abelian): a finitely generated torsion abelian group is finite (#15402)

Multramate committed 3 years ago

adeda57b

chore(measure_theory/tactic): remove the measurability attribute from two lemmas (#15295)

RemyDegenne committed 3 years ago

71d01152

feat(order/bounded_order): `is_well_order` instances for `with_top` and `with_bot` (#15278)

vihdzp committed 3 years ago

af213089

chore(category_theory/adjunction): fix a typo (#15720)

TwoFX committed 3 years ago

d3b1dbee

chore(topology/algebra/module, analysis/normed_space/linear_isometry): dedup `submodule.subtypeL` and `continuous_linear_map.subtype_val` (#15700)

ADedecker committed 3 years ago

cad19073