Commit 2025-12-09 12:40 0c56bb36

View on Github →

chore: missing API for toSpanSingleton (#32477) Adds:

LinearMap.toSpanSingleton_one_eq_algebraLinearMap
ContinuousLinearMap.toSpanSingleton_one_eq_algebraMapCLM
{LinearMap, ContinuousLinearMap}.smulRight_id Renames:
{LinearMap, ContinuousLinearMap}.toSpanSingleton_one -> .toSpanSingleton_apply_one
LinearMap.isIdempotentElem_apply_one_iff -> .isIdempotentElem_map_one_iff
algebraMapCLM_coe -> coe_algebraMapCLM
algebraMapCLM_toLinearMap -> toLinearMap_algebraMapCLM
ContinuousLinearMap.one_smulRight_eq_toSpanSingleton -> .smulRight_one_eq_toSpanSingleton

Estimated changes

Modified Mathlib/Algebra/Algebra/Bilinear.lean

added theorem LinearMap.toSpanSingleton_one_eq_algebraLinearMap

Modified Mathlib/Algebra/Module/CharacterModule.lean

Modified Mathlib/Algebra/Module/PID.lean

Modified Mathlib/Analysis/Calculus/Deriv/CompMul.lean

Modified Mathlib/LinearAlgebra/Span/Basic.lean

deleted theorem LinearMap.isIdempotentElem_apply_one_iff

added theorem LinearMap.isIdempotentElem_map_one_iff

added theorem LinearMap.smulRight_id

added theorem LinearMap.toSpanSingleton_apply_one

deleted theorem LinearMap.toSpanSingleton_one

Modified Mathlib/RingTheory/Ideal/Operations.lean

Modified Mathlib/RingTheory/SimpleModule/Basic.lean

Modified Mathlib/Topology/Algebra/Algebra.lean

added theorem ContinuousLinearMap.toSpanSingleton_one_eq_algebraMapCLM

deleted theorem algebraMapCLM_coe

deleted theorem algebraMapCLM_toLinearMap

added theorem coe_algebraMapCLM

added theorem toLinearMap_algebraMapCLM

Modified Mathlib/Topology/Algebra/Module/LinearMap.lean

deleted theorem ContinuousLinearMap.one_smulRight_eq_toSpanSingleton

added theorem ContinuousLinearMap.smulRight_id

added theorem ContinuousLinearMap.smulRight_one_eq_toSpanSingleton

added theorem ContinuousLinearMap.toSpanSingleton_apply_one

deleted theorem ContinuousLinearMap.toSpanSingleton_one

Modified Mathlib/Topology/ContinuousMap/Ideals.lean