Documentation Verification Report

Bilinear

📁 Source: FLT/Mathlib/Algebra/Algebra/Bilinear.lean

Statistics

Metric	Count
Definitions `mulLeft`, `mulRight`, `baseChangeRightOfAlgebraMap`, `baseChange_of_algebraMap`	4
Theorems `coe_mulLeft`, `coe_mulRight`, `baseChangeRightOfAlgebraMap_apply`, `baseChangeRightOfAlgebraMap_coe`, `baseChange_of_algebraMap_tmul`, `baseChange_of_algebraMap_tmul_left`, `baseChange_of_algebraMap_tmul_right`	7
Total	11

LinearEquiv

Definitions

Name	Category	Theorems
`mulLeft` 📖	CompOp	3 math math: `IsSimpleRing.mulLeft_det_eq_mulRight_det'`, `coe_mulLeft`, `MeasureTheory.algebra_ringHaarChar_eq_ringHaarChar_det`
`mulRight` 📖	CompOp	2 math math: `IsSimpleRing.mulLeft_det_eq_mulRight_det'`, `coe_mulRight`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_mulLeft` 📖	mathematical	—	`mulLeft`	—	—
`coe_mulRight` 📖	mathematical	—	`mulRight`	—	—

SemialgHom

Definitions

Name	Category	Theorems
`baseChangeRightOfAlgebraMap` 📖	CompOp	2 math math: `baseChangeRightOfAlgebraMap_coe`, `baseChangeRightOfAlgebraMap_apply`
`baseChange_of_algebraMap` 📖	CompOp	8 math math: `baseChange_of_algebraMap_tmul_right`, `IsDedekindDomain.FiniteAdeleRing.baseChange_bijective`, `baseChange_of_algebraMap_tmul_left`, `baseChangeRightOfAlgebraMap_coe`, `baseChangeRightOfAlgebraMap_apply`, `NumberField.InfiniteAdeleRing.baseChangeEquivAux_apply`, `NumberField.InfiniteAdeleRing.baseChangeEquivAux_coe_eq_baseChange_of_algebraMap`, `baseChange_of_algebraMap_tmul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`baseChangeRightOfAlgebraMap_apply` 📖	mathematical	—	`TensorProduct.RightActions.instAlgebra_fLT` `toRingHom` `baseChangeRightOfAlgebraMap` `baseChange_of_algebraMap`	—	`AlgHom.changeScalars_apply`
`baseChangeRightOfAlgebraMap_coe` 📖	mathematical	—	`TensorProduct.RightActions.instAlgebra_fLT` `toRingHom` `baseChangeRightOfAlgebraMap` `baseChange_of_algebraMap`	—	`baseChangeRightOfAlgebraMap_apply`
`baseChange_of_algebraMap_tmul` 📖	mathematical	—	`baseChange_of_algebraMap` `SemialgHom` `instFunLike`	—	—
`baseChange_of_algebraMap_tmul_left` 📖	mathematical	—	`baseChange_of_algebraMap`	—	`SemialgHomClass.toRingHomClass` `SemialgHomClass.instSemialgHom`
`baseChange_of_algebraMap_tmul_right` 📖	mathematical	—	`baseChange_of_algebraMap` `SemialgHom` `instFunLike`	—	—

---

← Back to Index