leanprover-community/mathlib

Pull Requests Commits

Update is_tensor_product.lean

erdOne committed 3 years ago

Verified 03399e9f

erdOne committed 3 years ago

c2a59f2b

feat(analysis/inner_product_space/two_dim): volume/area form of negated orientation (#16939)

hrmacbeth committed 3 years ago

5d7ab6e9

refactor(data/finset/noncomm_prod): Use `set.pairwise` (#16859)

YaelDillies committed 3 years ago

31263840

feat(data/multiset/basic): multiset inclusion is decidable (#16994)

eric-wieser committed 3 years ago

7121691d

feat(analysis/complex/open_mapping): the open mapping thm for holomorphic functions (#16780)

vbeffara committed 3 years ago

5c19b83b

feat(probability/independence): Kolmogorov's 0-1 law (#16648)

RemyDegenne committed 3 years ago

da4010c2

feat(topology/algebra/order/basic): `nhds_within` versions (#16956)

YaelDillies committed 3 years ago

e6f28f56

feat(topology/algebra/infinite_sum): generalize `tsum_le_of_sum_range_le` (#16951)

kex-y committed 3 years ago

f6b12763

fix(topology/metric_space/lipschitz): typo (#16962)

fpvandoorn committed 3 years ago

e623a7e4

refactor(combinatorics/young_tableau): move young diagram modules (#16954)

jakelev committed 3 years ago

34f53b6c

feat(topology/metric_space/emetric_space): `nhds_within` lemmas (#16952)

YaelDillies committed 3 years ago

4c2452e8

feat(analysis/normed_space/star/gelfand_duality): functoriality of `character_space ℂ` (#16835)

j-loreaux committed 3 years ago

e0ce2186

feat(analysis/bounded_variation): functions of bounded variation are ae differentiable (#16680)

sgouezel committed 3 years ago

71429ce7

feat(category_theory/groupoid/subgroupoid): subgroupoids and basic properties (#16742)

alreadydone committed 3 years ago

7a52b9ce

chore(scripts): update nolints.txt (#16968)

leanprover-community-bot committed 3 years ago

8f9520eb

refactor(geometry/euclidean/basic): rename `cospherical_subset` (#16947)

jsm28 committed 3 years ago

1e9b3df5

feat(analysis/inner_product_space/two_dim): new file (#16928)

hrmacbeth committed 3 years ago

a08db7e9

feat(measure_theory/group/prod): add properties for right-invariant measures (#16913)

fpvandoorn committed 3 years ago

ec247d43

feat(ring_theory/ideals/operations): add induction lemma (#16945)

AntoineChambert-Loir committed 3 years ago

9540b8cf

refactor(topology/sets/compacts): rename projection to is_compact (#16949)

fpvandoorn committed 3 years ago

95d4f658

chore(category_theory): put biproduct results on preadditive categories into the correct file (#16924)

javra committed 3 years ago

234ddfea

refactor(topology/continuous_function/{algebra, compact}): move `continuous_map.comp_right_alg_hom` (#16875)

j-loreaux committed 3 years ago

b68e4a89

feat(analysis/seminorm): seminorms are a `conditionally_complete_lattice` (#16582)

ADedecker committed 3 years ago

414df822

feat(analysis/normed_space/lp_equiv): equivalences between `lp` and `pi_Lp`, `bounded_continuous_function` (#15872)

j-loreaux committed 3 years ago

91b5bdde

chore(number_theory/number_field/basic): fix a name (#16943)

riccardobrasca committed 3 years ago

29761083

feat(ring_theory/dedekind_domain/ideal): height_one_spectrum is equivalent to maximal_spectrum (#16920)

Multramate committed 3 years ago

5147123e

feat(algebra/group_with_zero/units): add ring.inverse lemmas (#16889)

mariainesdff committed 3 years ago

9644d968

chore(algebra/order/sub): split file (#16868)

kim-em committed 3 years ago

02b85de4

chore(tactic/core): fix bug in `resolve_attribute_expr_list` (#16827)

hrmacbeth committed 3 years ago

938f1f1b

Older